FSM의 행위 일치 알고리즘을 이용한 임베디드 시스템의 합성적 안전성 분석 기법 = Compositional Safety Analysis for Embedded Systems using the FSM Behavioral Equivalence Algorithm

다국어 초록 (Multilingual Abstract)

As the embedded systems closely related with our living become complex by interoperating each other via internet, the safety issue of embedded systems begins to appear For checking safety properties of the system interactions, it is necessary to describe the system behaviors in formal methods and provide a systematic safety analysis technique. In this research, the behaviors of an embedded system are described by Labeled Transition Systems(LTS) and its safety properties are checked on the system model. For enhancing the existing compositional safety analysis technique, we perform the safety analysis techniques by checking the behavioral equivalence of the reduced model and a property model after reducing the system model in the viewpoint of the property.

국문 초록 (Abstract)

실생활과 밀접한 임베디드 시스템들이 인터넷에 연결되어 점차 복잡해지고 시스템 사용 패턴 또한 다양해짐에 따라 임베디드 시스템의 안전성 문제가 대두되고 있다. 임베디드 시스템의 상호작용에 대한 안전성을 분석하기 위서는 시스템 모델을 정형적으로 기술하고 이를 이용하는 체계적인 안전성 분석 방법이 필요하다. 이 연구에서는 Labeled Transition Systems (LTS)를 이용하여 시스템 모델과 속성 모델을 기술하고 안전성 속성이 만족되는지 검사하는 방법을 제공한다. 이 연구에서는 기존 합성적 안전성 분석 방법의 문제점을 해결하기 위해 시스템 모델을 속성모델 관점에서 축약하여 생성한 후에 두 모델 간의 행위 일치 관계를 이용하여 안전성 분석을 수행한다.

참고문헌 (Reference)

1 "The synthesis of sequential switching circuits Journal of Franklin Institute" 1954

2 "Synthesis of behavioral models from scenarios" 29 (29): 99-115, 2003

3 "Software safety analysis of a flight management system vertical navigation function- a status report" 2003

4 "Software intensive systems safety analysis" 19 (19): 21-26, 2004

5 "Safeware : System Safety and Computers" Addison-Wesley Publishing Company 1995

6 "Safety property verification using sequential SAT and bounded modeling checking" 21 (21): 132-143, 2004

7 "Safety models : an analytical tool for risk analysis of medical device systems" 445-451, 2001

8 "Proving properties of a safety-critical system" 41-50, 1991

9 "Methodology of independent software nuclear safety analysis of 5th International Symposium on Software Reliability Engineering" (v) : 76-83, 1994

10 "Communication and Concurrency" Prentice Hall

11 "Checking safety properties using compositional reachability analysis" 4978-, 1999

12 "A visual formalism for complex systems" 231-274, 1987