http://chineseinput.net/에서 pinyin(병음)방식으로 중국어를 변환할 수 있습니다.
변환된 중국어를 복사하여 사용하시면 됩니다.
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
함수 프로그램의 형추론 시스템은 에러검출과 디버깅을 위해 매우 가치있는 도구이다. 특히 형을 갖지않는 다형함수 프로그램에 형을 할당하는 시스템에 대한 연구가 계속되어 왔다. 이것은 프로그래머에게 형이 필요하지 않은 환경을 제공하기 위해 실행연산에 필요한 형정보를 추론해내는 시스템이다. 본 논문에서는 다형 언어가 제공하던 함수 언어의 융통성을 확대하기 위해 다중형 시스템을 도입하였다.
신승철(Seungcheol Shin) 한국정보보호학회 2006 情報保護學會誌 Vol.16 No.5
소프트웨어보안 분야는 정보보호, 소프트웨어공학, 프로그래밍언어 분야 등이 중첩되는 곳에 위치한다. 본 고는 프로그래밍언어 기술을 이용하여 소프트웨어 보안문제를 접근하는 한 예로서 정보흐름 보안성 분석법을 설명한다. 먼저 정보흐름 보안성이 관련되는 보안 문제들을 상기시킨 후에 이를 해결하는 프로그래밍언어 기술의 기본 개념들을 프로그램 분석법 중심으로 설명하고 최신 연구 경향을 소개한다.
증명보조기 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.
김은중(Eun-Jung Kim),신승철(Seungcheol Shin),조인준(In-June Jo) 한국콘텐츠학회 2022 한국콘텐츠학회논문지 Vol.22 No.11
화이트박스 테스팅은 블랙박스 테스팅과 달리 주어진 소스코드를 엄밀하게 분석하고 프로그램 동작을 예측함으로써 소프트웨어 오류를 검출하는 방법이다. 그 중에서 정적 분석은 프로그램 값의 근사 기법을 통해 실제 프로그램 동작을 포용함으로써 오류 여부를 예측할 수 있다. 또한 기호 실행은 각 실행 경로에 대한 경로 조건을 만족하는 프로그램 입력 값을 계산함으로써 오류를 발생하는 테스트 케이스를 생성할 수 있다. 하지만 정적 분석은 오탐이 많이 발생하거나 검출했더라도 결함의 근거를 제시하기 어렵다. 또한 기호 실행은 검출해야 하는 오류의 범위를 제어하거나 검출한 오류의 타입을 특정하기 어렵다. 이런 단점을 서로 보완하기 위해 두 기법의 융합을 고려할 수 있다. 본 논문은 화이트박스 테스팅 기법 중에서 정적 분석과 동적 기호 실행을 융합하여 정적 결함을 동적 오류로서 검산하는 방법과 심볼릭 테스팅을 통해 오류 검출 테스트 케이스를 생성하는 방법을 제시한다. 특히 두 개의 상용 도구를 융합하여 정적 결함의 동적 검산을 수행하면서 동시에 단위 테스트를 통해 테스트 커버리지를 얻어내는 결과를 보여준다. 두 도구를 융합하는 접착제는 정적 분석 결과로부터 결함을 검산할 수 있는 명세 코드를 삽입하는 모듈이다. 정적 결함 정보를 이용하여 해당 타입의 명세 패턴을 대입한 명세 코드를 생성하고 소스코드의 명세 위치에 삽입한다. 삽입된 소스코드를 심볼릭 테스팅 도구를 통해 단위 테스트를 수행하면 정적 결함에 해당하는 동적 오류를 발생시킬 수 있고 이때 얻어낸 테스트 케이스는 오류 검출 테스트 케이스가 된다. 이렇게 하면 정적 분석과 심볼릭 테스팅이 순차로 진행되면서 동시에 정적 결함의 검산과 오류의 근거 제시가 가능하다. White box testing can detect software errors by rigorously analyzing a given source code and anticipating its behaviours unlike black box testing. Static analysis as a white box testing can determine static defects by comprehending actual program behaviours with the approximation of program values. On the other, symbolic execution can generate test cases for dynamic errors by calculating program input which satisfy path conditions for each execution path. However static analysis gives a lot of false positives but shows not any proof for static defects. Symbolic execution cannot only identify types of dynamic errors but control the scope of errors. We need to consider a combined method of these techniques for making up these weaknesses. This paper shows a combined testing of static analysis and dynamic symbolic execution by representing how to validate static defects with dynamic errors and how to generate test cases of errors. We specify a method to combine two commercial tools, static analysis tool and symbolic testing tool which carry out the defects validation and unit testing simultaneously. The glue combining two tools is the instrumentation module by which source code is inserted with specification code for validating the corresponding error specification. The instrumented specification code is generated by being instantiated from specification patterns and inserted in the exact location for the corresponding error. With this instrumented source code the symbolic testing tool can execute unit testing and generate test cases for dynamic errors to validate static defects.
권민혁(Minhyuk Kwon),신승철(Seungcheol Shin) 한국정보과학회 2007 한국정보과학회 학술발표논문집 Vol.34 No.2C
산업자동화, 임베디드시스템, 지능형 빌딩, 유비쿼터스 환경 구축 등의 다양한 분야에 활용되는 PLC나 모션제어기를 위한 표준안은 IEC 61131-3이다. 이 표준안은 제어기를 위한 프로그래밍 환경과 언어의 문법구조를 정의하고 있으나, 도식적으로 표현되는 LD 프로그램의 저장 형식이 제시되지 않아서 관련 소프트웨어마다 서로 다른 저장 형식을 사용한다. PLCopen 그룹에서 배포한 표준 저장 형식 XML 스키마를 사용하면 데이터의 교환과 연동 언어들의 호환이 가능하다, 본 논문은 표준 XML 스키마를 기반하는 LD 그래픽편집기를 구현한다. 구현 형태는 Eclipse 플러그인으로서, Eclipse 도구인 EMF와 GEF를 이용하였다.