Abstract
Component-based Software Engineering (CBSE) is currently a key paradigm used for building safety-critical systems. Because these systems have to undergo a rigorous development and qualification process, one of the main challenges of introducing CBSE in this area is to ensure the integrity of the overall system after building it from reusable components. Many (formal) approaches for verification of compositions have been proposed, and they generally focus on behavioural integrity of components and their data semantics. An important aspect of this verification is a trade-off between scalability and completeness.
In this paper, we present a novel approach for verification of compositions for safety-critical systems, based on data semantics of components. We describe the composition and underlying safety-related properties of components as a Constraint Satisfaction Problem (CSP) and perform the verification by solving that problem. We show that CSP can be successfully applied for verification of compositions for many types of properties. In our experimental setup we also show how the proposed verification scales with regard to size of different system configurations.
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
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Adler, R., Schaefer, I., Trapp, M., Poetzsch-Heffter, A.: Component-based modeling and verification of dynamic adaptation in safety-critical embedded systems. ACM Trans. Embed. Comput. Syst. 10(2), 20:1–20:39 (2011), http://doi.acm.org/10.1145/1880050.1880056 , doi:10.1145/1880050.1880056
de Alfaro, L., Henzinger, T.A.: Interface automata. SIGSOFT Softw. Eng. Notes 26(5), 109–120 (2001), http://doi.acm.org/10.1145/503271.503226 , doi:10.1145/503271.503226
Apt, K.: Principles of Constraint Programming. Cambridge University Press, New York (2003)
Basu, A., Bensalem, S., Bozga, M., Combaz, J., Jaber, M., Nguyen, T.H., Sifakis, J.: Rigorous component-based system design using the bip framework. IEEE Software 28(3), 41–48 (2011), doi:10.1109/MS.2011.27
Benveniste, A., Caillaud, B., Nickovic, D., Passerone, R., Raclet, J.B., Reinkemeier, P., Sangiovanni-Vincentelli, A., Damm, W., Henzinger, T., Larsen, K. (2012) Contracts for Systems Design. Tech. rep., Research Report, Nr. 8147, Inria (November 2012)
Butz, H.: (-) Open integrated modular avionic (ima): State of the art and future development road map at airbus deutschland. Department of Avionic Systems at Airbus Deutschland GmbH Kreetslag 10, D-21129 Hamburg, Germany
choco Team, choco: an Open Source Java Constraint Programming Library. Research report 10-02-INFO, École des Mines de Nantes (2010)
Earle, C.B., Gómez-Martínez, E., Tonetta, S., Puri, S., Mazzini, S., Gilbert, J.L., Hachet, O., Oliver, R.S., Ekelin, C., Zedda, K.: Languages for Safety-Certification Related Properties. In: Proc. Work in Progress Session at 39th Euromicro Conf. on Software Engineering and Advanced Applications (SEAA 2013) (2013)
COMPASS (2011-2014) Compass - comprehensive modelling for advanced systems of systems, http://www.compass-research.eu
Crnkovic, I.: Building Reliable Component-Based Software Systems. Artech House, Inc., Norwood (2002)
Frey, P.: Case Study: Engine Control Application. Tech. rep., Ulmer Informatik-Berichte, Nr. 2010-03 (2010)
Gössler, G., Sifakis, J.: Composition for component-based modeling. Sci. Comput. Program 55(1-3), 161–183 (2005), http://dx.doi.org/10.1016/j.scico.2004.05.014 , doi:10.1016/j.scico.2004.05.014
Kindel, O., Friedrich, M.: Softwareentwicklung mit AUTOSAR: Grundlagen, Engineering, Management in der Praxis. dpunkt Verlag; Auflage: 1 (Juni 8, 2009)
Montano, G.: Dynamic reconfiguration of safety-critical systems: Automation and human involvement. PhD Thesis (2011)
SAFECER (2011-2015) Safecer - safety certification of software-intensive systems with reusable components, http://safecer.eu
Sentilles, S., Štěpán, P., Carlson, J., Crnković, I.: Integration of extra-functional properties in component models. In: Lewis, G.A., Poernomo, I., Hofmeister, C. (eds.) CBSE 2009. LNCS, vol. 5582, pp. 173–190. Springer, Heidelberg (2009), http://dx.doi.org/10.1007/978-3-642-02414-6_11
de Sousa, M.: Data-type checking of iec61131-3 st and il applications. In: 2012 IEEE 17th Conference on Emerging Technologies Factory Automation (ETFA), pp. 1–8 (2012), doi:10.1109/ETFA.2012.6489534
SPEEDS (2006-2012) Speculative and exploratory design in systems engineering - speeds, http://www.speeds.eu.com
Sun, X., Nuzzo, P., Wu, C.C., Sangiovanni-Vincentelli, A.: Contract-based system-level composition of analog circuits. In: 46th ACM/IEEE Design Automation Conference, DAC 2009, pp. 605–610. Los Alamitos (2009)
Tran, E.: Verification/validation/certification. Carnegie Mellon University, 18-849b Dependable Embedded Systems (1999)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this chapter
Cite this chapter
Kajtazovic, N., Preschern, C., Höller, A., Kreiner, C. (2015). Constraint-Based Verification of Compositions in Safety-Critical Component-Based Systems. In: Lee, R. (eds) Software Engineering, Artificial Intelligence, Networking and Parallel/Distributed Computing. Studies in Computational Intelligence, vol 569. Springer, Cham. https://doi.org/10.1007/978-3-319-10389-1_9
Download citation
DOI: https://doi.org/10.1007/978-3-319-10389-1_9
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-10388-4
Online ISBN: 978-3-319-10389-1
eBook Packages: EngineeringEngineering (R0)