FSM의 행위 일치 알고리즘을 이용한 임베디드 시스템의 합성적 안전성 분석 기법
Compositional Safety Analysis for Embedded Systems using the FSM Behavioral Equivalence Algorithm
0
조회
0
다운로드
2
인용
0
참고문헌
키워드
초록
실생활과 밀접한 임베디드 시스템들이 인터넷에 연결되어 점차 복잡해지고 시스템 사용 패턴 또한 다양해짐에 따라 임베디드 시스템의 안전성 문제가 대두되고 있다. 임베디드 시스템의 상호작용에 대한 안전성을 분석하기 위해서는 시스템 모델을 정형적으로 기술하고 이를 이용하는 체계적인 안전성 분석 방법이 필요하다. 이 연구에서는 Labeled Transition Systems (LTS)를 이용하여 시스템 모델과 속성 모델을 기술하고 안전성 속성이 만족되는지 검사하는 방법을 제공한다. 이 연구에서는 기존 합성적 안전성 분석 방법의 문제점을 해결하기 위해 시스템 모델을 속성모델 관점에서 축약하여 생성한 후에 두 모델 간의 행위 일치 관계를 이용하여 안전성 분석을 수행한다.
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.
참고문헌 (12)
- "Methodology of independent software nuclear safety analysis of 5th International Symposium on Software Reliability Engineering", (v), pp.76~83 (1994)
- "Safety models : an analytical tool for risk analysis of medical device systems", pp.445~451 (2001)
- "Software safety analysis of a flight management system vertical navigation function- a status report" (2003)
- "Software intensive systems safety analysis", 19(10), pp.21~26 (2004)
- "Safeware : System Safety and Computers" (1995), Addison-Wesley Publishing Company
- "Safety property verification using sequential SAT and bounded modeling checking", 21(2), pp.132~143 (2004)
- "Proving properties of a safety-critical system", pp.41~50 (1991)
- "Checking safety properties using compositional reachability analysis", pp.4978~ (1999)
- "Communication and Concurrency", Prentice Hall
- "Synthesis of behavioral models from scenarios", 29(2), pp.99~115 (2003)
- "The synthesis of sequential switching circuits Journal of Franklin Institute" (1954)
- "A visual formalism for complex systems", pp.231~274 (1987)