Formal verification of components assembly based on SysML and interface automata |
| |
Authors: | Samir Chouali Ahmed Hammad |
| |
Affiliation: | 1. Computer Science Laboratory, University of Franche Comt??, Besan?on, France
|
| |
Abstract: | We propose an approach which combines component SysML models and interface automata in order to assemble components and to verify formally their interoperability. So we propose
to verify formally the assembly of components specified with the expressive and semi-formal modeling language, SysML. We specify component-based system architecture with SysML Block Definition Diagram, and the composition links between components with Internal Block Diagrams. Component’s protocols
are specified with sequence diagrams, they are necessary to exploit interface automata formalism. Interface automata is a
common Input Output (I/O) automata-based formalism intended to specify the signature and the protocol level of the component
interfaces. We propose formal specifications for SysML semi-formal models in order to exploit interface automata approach. We also improve the interface automata approach by considering
system architecture, specified with SysML, in the verification of components composition. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|