A Contract-based Approach to Specifying and Verifying Safety Critical Systems |
| |
Authors: | Wei Dong Zhenbang Chen Ji Wang |
| |
Affiliation: | aNational Laboratory for Parallel and Distributed Processing ChangSha, P.R.China |
| |
Abstract: | Light-weight formal method has been regarded as an important approach to development of component-based safety critical systems. The paper proposes an approach which can formally specify and verify the contract of static structure, dynamic behavior and refinement of component systems based on UML 2.0 superstructure. As results, the correctness of static contract can be obtained via type checking of interfaces and connectors. Dynamic contract can be verified through determining the cooperativeness of integrated components, whose contracts are depicted with interface protocol state machines and their semantics models, namely contract automata. The refinement relation between high level component and its implementation will be guaranteed through defining the alternating simulation between contract automata of components at different levels. |
| |
Keywords: | formal specification software verification component-based software development |
本文献已被 ScienceDirect 等数据库收录! |