Abstract
The aim of this work is to propose a methodological approach to model and verify Component-Based Systems (CBS), directly from SysML requirement diagrams, and to ensure formally the architecture consistency of the specified systems. The architecture consistency is guaranteed, when the components that interact in CBS are compatible and all component requirements are preserved by the composition. We propose to exploit functional requirements of CBS, specified with SysML diagrams, and the composition of components to specify incrementally system architecture. Component interfaces are specified with SysML sequence diagrams to capture their behaviors (protocols). From a requirement diagram, we associate atomic requirements, represented as LTL properties, to reusable components satisfying them. LTL properties are verified on the components with SPIN model-checker. Then, we specify system architecture incrementally, with SysML Block Definition Diagram (BDD) and Internal Block Diagram (IBD), by treating, one by one the atomic requirements.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
We note that the term used in SysML for components is blocks.
- 2.
Blocks are instantiated as parts in IBD
References
The Object Management Group (OMG): OMG Systems Modeling Language (OMG SysML) Specification Version 1.2, June 2010. http://www.omg.org/spec/SysML/1.2/
Carrillo, O., Chouali, S., Mountassir, H.: Formalizing and verifying compatibility and consistency of sysml blocks. SIGSOFT Softw. Eng. Notes 37(4), 1–8 (2012)
Chouali, S., Hammad, A.: Formal verification of components assembly based on sysml and interface automata. ISSE 7(4), 265–274 (2011)
Lima, V., Talhi, C., Mouheb, D., Debbabi, M., Wang, L., Pourzandi, M.: Formal verification and validation of UML 2.0 sequence diagrams using source and destination of messages. Electron. Notes Theor. Comput. Sci. 254, 143–160 (2009)
de Alfaro, L., Henzinger, T.A.: Interface automata. In: Proceedings of the Ninth Annual Symposium on Foundations of Software Engineering (FSE), pp. 109–120. ACM Press (2001)
Object Management Group: The OMG Unified Modeling Language Specification, UML 2.0, July 2005
Lee, E.A., Xiong, Y.: A behavioral type system and its application in Ptolemy II. Formal Aspects Comput. 16(3), 210–237 (2004)
National Highway Traffic Safety Administration: Federal Motor Vehicle Safety Standards, September 1998
Holzmann, G.J.: Design and Validation of Computer Protocols. Prentice Hall, Englewood Cliffs (1991)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)
Pétin, J.F., Evrot, D., Morel, G., Lamy, P.: Combining SysML and formal methods for safety requirements verification. In: 22nd International Conference on Software & Systems Engineering and their Applications, Paris (2010)
van Lamsweerde, A.: From system goals to software architecture. In: Bernardo, M., Inverardi, P. (eds.) SFM 2003. LNCS, vol. 2804, pp. 25–43. Springer, Heidelberg (2003)
Barais, O., Duchien, L., Le Meur, A.F.: A framework to specify incremental software architecture transformations. In: 31st EUROMICRO Conference on Software Engineering and Advanced Applications, 2005, pp. 62–69 (2005)
Chen, Z., Liu, Z., Ravn, A.P., Stolz, V., Zhan, N.: Refinement and verification in component-based model-driven design. Sci. Comput. Program. 74(4), 168–196 (2009)
Dromey, R.G.: From requirements to design: Formalizing the key steps. In: Proceedings of the First International Conference on Software Engineering and Formal Methods, 2003, pp. 2–11 (2003)
Dromey, R.G.: Engineering large-scale software-intensive systems. In: ASWEC, pp. 4–6 (2007)
Lau, K.-K., Nordin, A., Rana, T., Taweel, F.: Constructing component-based systems directly from requirements using incremental composition. In: Proceedings of 36th EUROMICRO Conference on Software Engineering and Advanced Applications, pp. 85–93. IEEE (2010)
Farail, P., Goutillet, P., Canals, A., Le Camus, C., Sciamma, D., Michel, P., Cregut, X., Pantel, M.: The TOPCASED project : a toolkit in open source for critical aeronautic systems design. Ingénieurs de l’automobile 781, 54–59 (2006)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Carrillo, O., Chouali, S., Mountassir, H. (2014). Incremental Modeling of System Architecture Satisfying SysML Functional Requirements. In: Fiadeiro, J., Liu, Z., Xue, J. (eds) Formal Aspects of Component Software. FACS 2013. Lecture Notes in Computer Science(), vol 8348. Springer, Cham. https://doi.org/10.1007/978-3-319-07602-7_7
Download citation
DOI: https://doi.org/10.1007/978-3-319-07602-7_7
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-07601-0
Online ISBN: 978-3-319-07602-7
eBook Packages: Computer ScienceComputer Science (R0)