Formal verification of components assembly based on SysML and interface automata
Tóm tắt
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.
Tài liệu tham khảo
http://www.omg.org
http://www.incose.org
http://ap233.eurostep.com
http://www.uml.org
OMG (2003) UML for systems engineering. Request For Proposal
OMG (2006) OMG systems modeling language (OMG SysML) specification, OMG Final Adopted Specification. http://www.omgsysml.org
Adler TB, De Alfaro L, Da Silva RD, Faella M, Legay A, Raman V, Roy P (2006) Ticc, a tool for interface compatibility and composition. In: In Proceedings 18th international conference on computer aided verification (CAV), of lecture notes in computer science, vol 4144. Springer, New York, pp 59–62
Alfaro L, Henzinger TA (2001) Interface automata. In: 9th annual symposium on foundations of software engineering. FSE, ACM Press, New York, pp 109–120
Alfaro L, Henzinger TA (2005) Interface-based design. In: Broy M, Gruenbauer J, Harel D, Hoare CAR (eds) Engineering theories of software-intensive systems. NATO science series: Math Phys Chem, vol 195. Springer, New York, pp 83–104
Alfaro L, Henzinger TA, Stoelinga M (2002) Timed interfaces. In: EMSOFT ’02: proceedings of the second international conference on embedded software. Springer, London, pp 108–122
Baille G, Garnier P, Mathieu H, Pissard-Gibollet R (1999) The INRIA Rhône-Alpes CyCab. Technical report, INRIA, Describes the package natbib
Carneiro E, Maciel P, Callou G, Tavares E, Nogueira B (2008) Mapping SysML state machine diagram to time petri net for analysis and verification of embedded real-time systems with energy constraints. Electr Micro Electr Int Confer Adv 0: 1–6
Heineman GT, Councill WT (2001) Component based Software engineering. Addison Wesley, Boston
Jarraya Y, Debbabi M, Bentahar J (2009) On the Meaning of SysML Activity Diagrams. In: Proceedings of the 2009 16th annual IEEE international conference and workshop on the engineering of computer based systems, ECBS ’09. IEEE Computer Society, Washington, DC, pp 95–105
Knorreck D, Apvrille L, de Saqui-Sannes P (2011) TEPE: a SysML language for time-constrained property modeling and formal verification. SIGSOFT Softw Eng Notes 36: 1–8
Konstantas D (1995) Interoperation of object oriented application. In: Nierstrasz O, Tsichritzis D (eds) Object-oriented software composition. Prentice Hall, Upper Saddle River, pp 69–95
Lynch N, Tuttle M (1987) Hierarchical correctness proofs for distributed algorithms. In: 6th ACM symposium on principles of distributed computing. ACM Press, Florida, pp 137–151
Pétin J-F, Evrot D, Morel G, Lamy P (2010) Combining SysML and formal methods for safety requirements verification. In: 22nd International Conference on Software and Systems Engineering and their Applications, CDROM, vol 12. Paris, France
Szyperski C (1999) Component software. ACM Press/Addison-Wesley, New York
Wang R, Dagli CH (2008) An executable system architecture approach to discrete events system modeling using SysML in conjunction with colored Petri Net. In: Systems conference, 2nd annual IEEE, 2008
de Wegner P (1996) Interoperability. ACM Comput Surv 28(1): 285–287