Abstract
Undesired feature interaction may lead to safety-critical behavior in cyber-physical systems (CPSs). For specifying feature coordination of a cyber-physical software system (i.e., its cyber-part), an approach based on the Situation Calculus was previously published. However, no verification of the feature coordination in the physical environment was possible in spite of its formal specification. Verification of (safety-critical) feature coordination in CPSs is important, however, and requires additional models.
This paper shows that a specification of feature coordination can be formally verified against a safety-relevant property, when combined with an additional (simple) physical model and a model of an independent embodied entity in the environment. These models are qualitative and intended to be minimalist, in order to facilitate formal and tool-supported verification. We demonstrate formal verification of the combined model twice, through model-checking a representation in synchronized finite-state machines against the property formulated in time logic, and through a planner with an inverted goal condition, based on a systematically derived model in Fluent Calculus. The results of verification are consistent, and we contrast and discuss both approaches. In summary, we present formal verification of cyber-physical feature coordination with minimalist qualitative models.
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
Similar content being viewed by others
Notes
- 1.
ECLiPSe Constraint Programming System: http://www.eclipseclp.org.
References
Apel, S., Batory, D., Kästner, C., Saake, G.: Feature-Oriented Software Product Lines: Concepts and Implementation. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-37521-7
Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)
Bensalem, S., Havelund, K., Orlandini, A.: Verification and validation meetplanning and scheduling. Int. J. Softw. Tools Technol. Transf. 16(1), 1–12 (2014). https://doi.org/10.1007/s10009-013-0294-x
Bocovich, C., Atlee, J.M.: Verification and validation meetplanning and scheduling. In: Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE 2014, pp. 553–563. ACM, New York (2014). https://doi.org/10.1145/2635868.2635927
Ertl, D., Dominka, S., Kaindl, H.: Using a mediator to handle undesired feature interaction of automated driving. In: 2013 IEEE International Conference on Systems, Man, and Cybernetics, pp. 4555–4560, October 2013. https://doi.org/10.1109/SMC.2013.775
Hoch, R., Kaindl, H.: Verification of feature coordination using the fluent calculus. In: Damiani, E., Spanoudakis, G., Maciaszek, L.A. (eds.) Proceedings of the 13th International Conference on Evaluation of Novel Approaches to Software Engineering, ENASE 2018, Funchal, Madeira, Portugal, 23–24 March 2018, pp. 169–179. SciTePress (2018). https://doi.org/10.5220/0006771401690179
Hoch, R., Kaindl, H., Popp, R., Ertl, D., Horacek, H.: Semantic service specification for V&V of service composition and business processes. In: Proceedings of the 48th Annual Hawaii International Conference on System Sciences (HICSS-48). IEEE Computer Society Press, Piscataway (2015)
ISO 26262: ISO 26262, road vehicles - functional safety, November 2011
Jackson, M., Zave, P.: Distributed feature composition: a virtual architecture for telecommunications services. IEEE Trans. Softw. Eng. (TSE) 24(10), 831–847 (1998)
Juarez-Dominguez, A.L., Day, N.A., Joyce, J.J.: Modelling feature interactions in the automotive domain. In: Proceedings of the International Workshop on Models in Software Engineering, MiSE 2008, pp. 45–50. ACM, New York (2008). https://doi.org/10.1145/1370731.1370743
Kropf, T.: Introduction to Formal Hardware Verification. Springer, Heidelberg (1999). https://doi.org/10.1007/978-3-662-03809-3
Levesque, H.J., Reiter, R., Lespèrance, Y., Lin, F., Scherl, R.B.: GOLOG: a logic programming language for dynamic domains. J. Log. Program. 31(1), 59–83 (1997). https://doi.org/10.1016/S0743-1066(96)00121-5. http://www.sciencedirect.com/science/article/pii/S0743106696001215
Luckeneder, C., Kaindl, H.: Systematic top-down design of cyber-physical models with integrated validation and formal verification. In: 40th International Conference on Software Engineering Companion, ICSE 2018 Companion. ACM (2018)
McCarthy, J., Hayes, P.J.: Some philosophical problems from the standpoint of artificial intelligence. In: Meltzer, B., Michie, D. (eds.) Machine Intelligence, vol. 4, pp. 463–502. Edinburgh University Press, Edinburgh (1969)
Nilsson, N.J.: Principles of Artificial Intelligence. Springer, Heidelberg (1982)
NuSMV: NuSMV: a new symbolic model checker, October 2018. http://nusmv.fbk.eu/
Rathmair, M., Luckeneder, C., Kaindl, H.: Minimalist qualitative models for model checking cyber-physical feature coordination. In: Proceedings of the 23rd Asia-Pacific Software Engineering Conference (APSEC). IEEE, December 2016
Reiter, R.: The frame problem in situation the calculus: a simple solution (sometimes) and a completeness result for goal regression. In: Lifschitz, V. (ed.) Artificial Intelligence and Mathematical Theory of Computation, pp. 359–380. Academic Press Professional Inc., San Diego (1991). http://dl.acm.org/citation.cfm?id=132218.132239
Schiffel, S., Thielscher, M.: Interpreting golog programs in flux. In: 7th International Symposium On Logical Formalizations of Commonsense Reasoning. The AAAI Press (2005)
Schramm, D., Bardini, R., Hiller, M.: Vehicle Dynamics. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-540-36045-2
Simko, G., Jackson, E.K.: A bounded model checking tool for periodic sample-hold systems. In: Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control, pp. 157–162. ACM (2014)
Sivaji, V., Sailaja, M.: Adaptive cruise control systems for vehicle modeling using stop and go manoeuvres. Int. J. Eng. Res. Appl. (IJERA) 3, 2248–9622 (2013). ISSN
Thielscher, M.: Introduction to the fluent calculus. Electron. Trans. Artif. Intell. 2, 179–192 (1998)
Thielscher, M.: FLUX: a logic programming method for reasoning agents. Theory Pract. Log. Program. 5(4–5), 533–565 (2005)
Wagner, D., Kaindl, H., Dominka, S., Dübner, M.: Optimization of feature interactions for automotive combustion engines. In: Proceedings of the 31st Annual ACM Symposium on Applied Computing, pp. 1401–1406. ACM (2016)
Winner, H., Schopper, M.: Adaptive cruise control. In: Winner, H., Hakuli, S., Lotz, F., Singer, C. (eds.) Handbuch Fahrerassistenzsysteme. A, pp. 851–891. Springer, Wiesbaden (2015). https://doi.org/10.1007/978-3-658-05734-3_46
Acknowledgments
The FeatureOpt project (No. 849928) has been partially funded by the Austrian Federal Ministry of Transport, Innovation and Technology (BMVIT) under the program “ICT of the Future” between June 2015 and May 2018. More information can be found at https://iktderzukunft.at/en/.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Kaindl, H., Hoch, R., Rathmair, M., Luckeneder, C. (2019). Formal Verification of Cyber-physical Feature Coordination with Minimalist Qualitative Models. In: Damiani, E., Spanoudakis, G., Maciaszek, L. (eds) Evaluation of Novel Approaches to Software Engineering. ENASE 2018. Communications in Computer and Information Science, vol 1023. Springer, Cham. https://doi.org/10.1007/978-3-030-22559-9_12
Download citation
DOI: https://doi.org/10.1007/978-3-030-22559-9_12
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-22558-2
Online ISBN: 978-3-030-22559-9
eBook Packages: Computer ScienceComputer Science (R0)