Formal verification of an automotive scenario in service-oriented computing

ABSTRACT

We report on the successful application of academic experience with formal modelling and verification techniques to an automotive scenario from the service-oriented computing domain. The aim of this industrial case study is to verify a priori, thus before implementation, certain design issues. The specific scenario is a simplified version of one of possible new services for car drivers to be provided by the in-vehicle computers.

REFERENCES

• 1: Christel Baier , Lucia Cloth , Boudewijn Haverkort , Matthias Kuntz , Markus Siegle, Model Checking Action- and State-Labelled Markov Chains, Proceedings of the 2004 International Conference on Dependable Systems and Networks, p.701, June 28-July 01, 2004
• 2: Maurice H. ter Beek , Stefania Gnesi , Franco Mazzanti , Corrado Moiso, Formal Modelling and Verification of an Asynchronous Extension of SOAP, Proceedings of the European Conference on Web Services, p.287-296, December 04-06, 2006 [doi>10.1109/ECOWS.2006.22]
• 3: M.H. ter Beek, A. Fantechi, S. Gnesi and F. Mazzanti. An action/state-based model-checking approach for the analysis of communication protocols for Service-Oriented Applications. To appear in Proceedings of the 12th International Workshop on Formal Methods for Industrial Critical Systems (FMICS'07), Berlin, Germany, volume 4916 of Lecture Notes in Computer Science. Springer, Berlin, 2008.
• 4: Girish Bhat , Rance Cleaveland , Orna Grumberg, Efficient On-the-Fly Model Checking for CTL, Proceedings of the 10th Annual IEEE Symposium on Logic in Computer Science, p.388, June 26-29, 1995
• 5: S. Chaki, E.M. Clarke, J. Ouaknine, N. Sharygina and N. Sinha. Concurrent software verification with states, events, and deadlocks. Formal Aspects of Computing 17(4): 461--483, 2005.
• 6: E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.244-263, April 1986 [doi>10.1145/5397.5399]
• 7: Rocco De Nicola , Joost-Pieter Katoen , Diego Latella , Michele Loreti , Mieke Massink, Model checking mobile stochastic logic, Theoretical Computer Science, v.382 n.1, p.42-70, August, 2007 [doi>10.1016/j.tcs.2007.05.008]
• 8: Rocco De Nicola , Frits Vaandrager, Action versus state based logics for transition systems, Proceedings of the LITP spring school on theoretical computer science on Semantics of systems of concurrent processes, p.407-419, November 1990, La Roche Posay, France
• 9: Rocco De Nicola , Frits Vaandrager, Three logics for branching bisimulation, Journal of the ACM (JACM), v.42 n.2, p.458-487, March 1995 [doi>10.1145/201019.201032]
• 10: A. Fantechi, S. Gnesi, A. Lapadula, F. Mazzanti, R. Pugliese and F. Tiezzi. A model checking approach for verifying COWS specifications. To appear in Proceedings of the 11th Conference on Fundamental Approaches to Software Engineering (FASE'08), Budapest, Hungary, Lecture Notes in Computer Science. Springer, Berlin, 2008.
• 11: Jean-Claude Fernandez , Claude Jard , Thierry Jéron , César Viho, Using On-The-Fly Verification Techniques for the Generation of test Suites, Proceedings of the 8th International Conference on Computer Aided Verification, p.348-359, August 03, 1996
• 12: P. Gagnon, F. Mokhati and M. Badri. Applying Model Checking to Concurrent UML Models. Journal of Object Technology 7(1):59--84, 2008.
• 13: S. Gnesi and F. Mazzanti. On the y model checking of communicating UML State Machines. In Proceedings of the 2nd International Conference on Software Engineering Research, Management & Applications (SERA'04), Los Angeles, CA, USA, pages 331--338, 2004.
• 14: S. Gnesi and F. Mazzanti. A Model Checking Verification Environment for UML Statecharts. Presented at the XLIII Annual Italian Conference AICA, Udine, 2005.
• 15: L. Gönczy and D. Varró. Model-Driven Transformations for Deployment|Prototype. Sensoria Deliverable 6.4a, September 2007. Available via {31}.
• 16: Matthew Hennessy , Robin Milner, Algebraic laws for nondeterminism and concurrency, Journal of the ACM (JACM), v.32 n.1, p.137-161, Jan. 1985 [doi>10.1145/2455.2460]
• 17: Holger Hermanns , Joost-Pieter Katoen , Joachim Meyer-Kayser , Markus Siegle, Towards Model Checking Stochastic Process Algebra, Proceedings of the Second International Conference on Integrated Formal Methods, p.420-439, November 01-03, 2000
• 18: Michael Huth , Radha Jagadeesan , David A. Schmidt, Modal Transition Systems: A Foundation for Three-Valued Program Analysis, Proceedings of the 10th European Symposium on Programming Languages and Systems, p.155-169, April 02-06, 2001
• 19: Ekkart Kindler , Tobias Vesper, ESTL: A Temporal Logic for Events and States, Proceedings of the 19th International Conference on Application and Theory of Petri Nets, p.365-384, June 22-26, 1998
• 20: Alexander Knapp , Stephan Merz , Christopher Rauh, Model Checking - Timed UML State Machines and Collaborations, Proceedings of the 7th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems: Co-sponsored by IFIP WG 2.2, p.395-416, September 09-12, 2002
• 21: A. Knapp and G. Zhang. Model Transformations for Integrating and Validating Web Application Models. In H.C. Mayr and R. Breu, editors, Proceedings of Modellierung 2006 (MOD'06), Innsbruck, Austria, volume 82 of Lecture Notes in Informatics, pages 115--128. Gesellschaft fur Informatik, Bonn, 2006.
• 22: N. Koch and D. Berndl. Requirements Modelling and Analysis of Selected Scenarios of the Automative Case Study. Sensoria Deliverable 8.2a, September 2007. Available via {31}.
• 23: N. Koch, P. Mayer, R. Heckel, L. Günczy and C. Montangero. UML for Service-Oriented Systems. Sensoria Deliverable 1.4a, September 2007. Available via {31}.
• 24: P. Liggesmeyer, M. Rothfelder, M. Rettelbach and T. Ackermann. Qualitätssicherung Software-basierter Technischer Systeme-Problembereiche und Lösungsans ätze. Informatik Spektrum, 21(5):249--258, 1998.
• 25: Zohar Manna , Amir Pnueli, The temporal logic of reactive and concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1992
• 26: F. Mazzanti. UMC User Guide v3.3. Technical Report 2006-TR-33, Istituto di Scienza e Tecnologie dell'Informazione \A. Faedo", CNR, 2006. http://fmt.isti.cnr.it/WEBPAPER/UMC-UG33.pdf
• 27: Robert Meolic , Tatjana Kapus , Zmago Brezočnik, ACTLW - An action-based computation tree logic with unless operator, Information Sciences: an International Journal, v.178 n.6, p.1542-1557, March, 2008 [doi>10.1016/j.ins.2007.10.023]
• 28: Markus Müller-Olm , David A. Schmidt , Bernhard Steffen, Model-Checking: A Tutorial Introduction, Proceedings of the 6th International Symposium on Static Analysis, p.330-354, September 22-24, 1999
• 29: A. Saad. Java-based Functionality and Data Management in the automobile|Prototyping at BMW Car IT GmbH. JavaSPEKTRUM. SIGS Datacom, March 2003.
• 30: SCADE suite. http://www.estereltechnologies. com/products/scade-suite/
• 31: EU project Sensoria (IST-2005-016004). http://www.sensoria-ist.eu/
• 32: SPARK toolset. http://www.praxis-his.com/sparkada/
• 33: Spin model checker. http://www.spinroot.com
• 34: UMC model checker. http://fmt.isti.cnr.it/umc/
• 35: Unified Modeling Language. http://www.uml.org/
• 36: Uppaal tool. http://www.uppaal.com
• 37: M. Wirsing, A. Clark, S. Gilmore, M. Hölzl, A. Knapp, N. Koch and A. Schroeder. Semantic-Based Development of Service-Oriented Systems. In E. Najm, J.-F. Pradat-Peyre and V. Donzeau-Gouge, editors, Proceedings of the 26th International Conference on Formal Techniques for Networked and Distributed Systems (FORTE'06), Paris, France, volume 4229 of Lecture Notes in Computer Science, pages 24--45. Springer, Berlin, 2006.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Model checking

General Terms:
Experimentation, Verification

Keywords:
automotive systems, model checking, service-oriented computing