http://chineseinput.net/에서 pinyin(병음)방식으로 중국어를 변환할 수 있습니다.
변환된 중국어를 복사하여 사용하시면 됩니다.
증명보조기 Coq을 이용한 래더 다이어그램 의미구조의 정형화
신승철(Seungcheol Shin) 한국정보과학회 2010 정보과학회논문지 : 소프트웨어 및 응용 Vol.37 No.1
산업자동화 분야에는 특수목적 마이크로콘트롤러인 PLC가 널리 사용된다. PLC 프로그램 분석과 검증을 위한 연구에서 우선적으로 해야 할 일은 PLC 프로그래밍 언어의 의미구조를 정형적으로 제시하는 것이다. 본 논문은 PLC 프로그래밍에 널리 사용하는 LD 언어의 의미구조를 정의한다. LD 언어는 그래픽 언어이기 때문에 먼저 텍스트 언어 Symbolic LD로 구문구조를 정형화한 다음에, Symbolic LD에 대한 의미구조를 정의할 수가 있다. 본 논문은 Symbolic LD의 의미구조를 자연 의미구조 기법으로 정의하고, 증명 보조기 Coq을 이용하여 정형화하였다. Special-purpose microcontrollers PLCs have been widely used in the area of industrial automation. For the research of analysis and verification for PLC programs, first of all we have to specify formal sematics of PLC programming languages. This paper defines formally the operational semantics of LD language. After we transform the graphical language LD into its textual representation Symbolic LD, we give semantics of Symbolic LD since LD language is a graphical language. This paper defines the natural sematics of Symbolic LD and formalizes it in Coq proof assistant.
신승철(Seungcheol Shin) 한국정보보호학회 2006 情報保護學會誌 Vol.16 No.5
소프트웨어보안 분야는 정보보호, 소프트웨어공학, 프로그래밍언어 분야 등이 중첩되는 곳에 위치한다. 본 고는 프로그래밍언어 기술을 이용하여 소프트웨어 보안문제를 접근하는 한 예로서 정보흐름 보안성 분석법을 설명한다. 먼저 정보흐름 보안성이 관련되는 보안 문제들을 상기시킨 후에 이를 해결하는 프로그래밍언어 기술의 기본 개념들을 프로그램 분석법 중심으로 설명하고 최신 연구 경향을 소개한다.
46-3Q 촉매 상에서 폐플라스틱의 열분해 오일로부터 수소 제조
신승철(SEUNGCHEOL SHIN),정하늘(HANEUL JUNG),한단비(DANBEE HAN),백영순(YOUNGSOON BAEK) 한국수소및신에너지학회 2023 한국수소 및 신에너지학회논문집 Vol.34 No.6
Pyrolysis oil (C5-C20) produced using plastic non-oxidative pyrolysis technology produces naphtha oil (C5-C10) through a separation process, and naphtha oil produces hydrogen through a reforming reaction to secure economic efficiency and social and environmental benefits. In this study, waste plastic pyrolysis oil was subjected to a steam reforming reaction on a commercialized catalyst of 46-3Q And it was found that the 46-3Q catalyst reformed the pyrolysis oil to produce hydrogen. Therefore, an experiment was performed to increase hydrogen yield and minimize the byproduct of ethylene. The reaction experiment was performed using actual waste plastic oil (C8-C11) with temperature, steam/carbon ratio (S/C) ratio, and space velocity as variables. We studied reaction conditions that can maximize hydrogen yield and minimize ethylene byproducts.
신승철(Seungcheol Shin),김상도(Sangdo Kim),유원희(Weonhee Yoo) 한국정보과학회 1988 한국정보과학회 학술발표논문집 Vol.15 No.1
함수 프로그램의 형추론 시스템은 에러검출과 디버깅을 위해 매우 가치있는 도구이다. 특히 형을 갖지않는 다형함수 프로그램에 형을 할당하는 시스템에 대한 연구가 계속되어 왔다. 이것은 프로그래머에게 형이 필요하지 않은 환경을 제공하기 위해 실행연산에 필요한 형정보를 추론해내는 시스템이다. 본 논문에서는 다형 언어가 제공하던 함수 언어의 융통성을 확대하기 위해 다중형 시스템을 도입하였다.
한반도 후기 플라이스토세 퇴적층에서 관찰되는 fish burrow에 관한 연구
신승원(Seungwon Shin),김진철(Jin Cheul Kim),하수진(Sujin Ha),박승철(Seungcheol Park),정대교(Daekyo Cheong),채용운(Yongun Chae),김영준(Youngjun Kim),김우락(Woorak Kim),이진영(Jin-Young Lee),남욱현(Wookhyun Nahm),임현수(Hyoun Soo Lim) 대한지질학회 2021 대한지질학회 학술대회 Vol.2021 No.10
홍천강 일대는 하안단구가 발달하고 단구면을 따라 후기 구석기 유적이 다수 분포하고 있다. 기존 연구에 따르면 대부분 5만년 이후의 후기 구석기 유적으로 보고되고 있으나 이번 연구에서는 MIS 5 시기에 해당하는 구석기 유적이 발견되었으며, 2매의 수직 방향으로 발달하는 매우 특이한 구조가 관찰되었다. 연구를 위하여 대표 퇴적단면을 선정하여, 연대학적, 퇴적학적, 지구화학적 분석을 수행하였고, 2매의 수직 구조에 대하여 수직 길이와 직경과 단경을 측정하였다. 총 5 m의 퇴적단면에서 최하부는 자갈층이 관찰되었고, 약 2.5m 구간까지 상향세립화 경향성이 확인되었다. 그리고 이후 구간에서는 약 10% 내외의 모래를 포함하는 머드층이 비교적 균질하게 관찰되었다. 또한, 총 6개의 OSL 연대를 측정하였는데, 하부의 모래층에서는 연대 측정 범위를 넘어 측정이 되지 않았고, 이후 4개의 시료에서는 fine-grain을 이용한 연대를 측정하여 101~133 ka 구간의 퇴적시기를 획득하였다. 이러한 결과들을 종합하였을 때, 하부에 하천에 의하여 형성된 자갈과 모래 사주 위에 범람원 퇴적층이 발달한 것으로 해석된다. 수직으로 발달하는 구조는 상부층에서 2매가 반복적으로 관찰되었으며, 수직 길이는 최대 50 cm까지 나타난다. 상부층(190)과 하부층(133)에서 장축과 단축을 측정한 결과, 상부층은 장축이 3.4 cm, 단축이 2.56 cm, 하부층의 장축이 2.53 cm, 단축이 1.91 cm 로 상부층의 구조가 조금 큰 것으로 측정되었다. 그리고 두 층에서의 장축과 단축의 비는 각각 1.34, 1.35로 같은 구조일 가능성이 높은 것으로 사료된다. 그동안 한반도에서의 플라이스토세 퇴적층 내에 수직으로 발달하는 구조는 설치류에 의한 구조, 지렁이와 같은 worm burrow, 혹은 식물 뿌리 등에 의한 구조들이 보고되었다. 그러나 이번에 관찰되는 수직 구조와는 크기 차이가 현저하여 가능성이 낮은 것으로 판단된다. 따라서 이번 연구에서 관찰되는 수직의 구조는 어류에 의한 구조일 가능성이 높은 것으로 해석되고 한반도를 비롯하여 동아시아 일대에 서식하고 논과 같은 환경에서 수직으로 굴을 파고 서식하는 드렁허리와 가장 유사한 것으로 판단된다.