Maurice H. ter Beek
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.
- C. Baier, L. Cloth, B. Haverkort, M. Kuntz and M. Siegle. Model checking action- and state-labelled Markov chains. In Proceedings of the International Conference on Dependable Systems and Networks (DSN'04), Florence, Italy, pages 701--710. IEEE Computer Society, Los Alamitos, CA, 2004. Google Scholar
Digital Library
- M.H. ter Beek, S. Gnesi, F. Mazzanti and C. Moiso. Formal Modelling and Verification of an Asynchronous Extension of SOAP. In A. Bernstein, T. Gschwind and W. Zimmermann, editors, Proceedings of the 4th IEEE European Conference on Web Services (ECOWS'06),Zurich, Switzerland, pages 287--296. IEEE Computer Society, Los Alamitos, CA, 2006. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- G. Bhat, R. Cleaveland and O. Grumberg. Efficient On-the-Fly Model Checking for CTL*. In Proceedings of the 10th IEEE Symposium on Logics in Computer Science (LICS'95), San Diego, CA, USA, pages 388--397. IEEE Computer Society, Los Alamitos, CA, 1995. Google ScholarDigital Library
- 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.Google ScholarCross Ref
- E.M. Clarke, E.A. Emerson and A.P. Sistla. Automatic Verification of Finite State Concurrent Systems using Temporal Logic Specifications. ACM Transactions on Programming Languages and Systems 8(2): 244--263, 1986. Google ScholarDigital Library
- R. De Nicola, J.-P. Katoen, D. Latella, M. Loreti and M. Massink. Model checking mobile stochastic logic. Theoretical Computer Science 382(1): 42--70, 2007. Google ScholarDigital Library
- R. De Nicola and F.W. Vaandrager. Actions versus State based Logics for Transition Systems. In I. Guessarian, editor, Proceedings Spring School on Semantics of Systems of Concurrent Processes, La Roche Posay, France, volume 469 of Lecture Notes in Computer Science, pages 407--419. Springer, Berlin, 1990. Google ScholarDigital Library
- R. De Nicola and F.W. Vaandrager. Three Logics for Branching Bisimulation. Journal of the ACM 42(2): 458--487, 1995. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- J.-C. Fernandez, C. Jard, T. Jéron and C. Viho. Using On-The-Fly Verification Techniques for the Generation of test Suites. In R. Alur and T.A. Henzinger, editors, Proceedings of the 8th International Conference on Computer-Aided Verification (CAV'96), New Brunswick, NJ, USA, volume 1102 of Lecture Notes in Computer Science, pages 348--359. Springer, Berlin, 1996. Google ScholarDigital Library
- P. Gagnon, F. Mokhati and M. Badri. Applying Model Checking to Concurrent UML Models. Journal of Object Technology 7(1):59--84, 2008.Google ScholarCross Ref
- 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.Google Scholar
- S. Gnesi and F. Mazzanti. A Model Checking Verification Environment for UML Statecharts. Presented at the XLIII Annual Italian Conference AICA, Udine, 2005.Google Scholar
- L. Gönczy and D. Varró. Model-Driven Transformations for Deployment|Prototype. Sensoria Deliverable 6.4a, September 2007. Available via {31}.Google Scholar
- M. Hennessy and R. Milner. Algebraic Laws for Nondeterminism and Concurrency. Journal of the ACM 32(1): 137--161, 1985. Google ScholarDigital Library
- H. Hermanns, J.-P. Katoen, J. Meyer-Kayser and M. Siegle. Towards model checking stochastic process algebra. In W. Grieskamp, T. Santen and B. Stoddart, editors, Proceedings of the 2nd International Conference on Integrated Formal Methods (IFM'00), Dagstuhl, Wadern, Germany, volume 1945 of Lecture Notes in Computer Science, pages 420--439. Springer, Berlin, 2000. Google ScholarDigital Library
- M. Huth, R. Jagadeesan and D.A. Schmidt. Modal Transition Systems: A Foundation for Three-Valued Program Analysis. In D. Sands, editor, Programming Languages and Systems|Proceedings of the 10th European Symposium on Programming (ESOP'01), Genova, Italy, volume 2028 of Lecture Notes in Computer Science, pages 155--169. Springer, Berlin, 2001. Google ScholarDigital Library
- E. Kindler and T. Vesper. ESTL: A Temporal Logic for Events and States. In J. Desel and M. Silva, editors, Proceedings of the 19th International Conference on Application and Theory of Petri Nets (ICATPN'98), Lisbon, Portugal, volume 1420 of Lecture Notes in Computer Science, pages 365--384. Springer, Berlin, 1998. Google ScholarDigital Library
- A. Knapp, S. Merz and Ch. Rauh. Model Checking-Timed UML State Machines and Collaborations. In W. Damm and E.-R. Olderog, editors, Proceedings of the 7th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT'02), Oldenburg, Germany, volume 2469 of Lecture Notes in Computer Science, pages 395--414. Springer, Berlin, 2002. See also http://www.pst.ifi.lmu.de/projekte/hugo/ Google ScholarDigital Library
- 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 für Informatik, Bonn, 2006.Google Scholar
- 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}.Google Scholar
- 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}.Google Scholar
- 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.Google ScholarCross Ref
- Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems-Specification. Springer, Berlin, 1992. Google ScholarDigital Library
- 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.pdfGoogle Scholar
- R. Meolic, T. Kapus and Z. Brezočnik. ACTLW - An action-based computation tree logic with unlessoperator. Information Sciences 178(6): 1542--1557, 2008. Google ScholarDigital Library
- M. Müller-Olm, D.A. Schmidt and B. Steffen. Model-Checking-A Tutorial Introduction. In A. Cortesi and G. Filé, editors, Proceedings of the 6th International Symposium on Static Analysis (SAS'99), Venice, Italy, volume 1694 of Lecture Notes in Computer Science, pages 330--354. Springer, Berlin, 1999. Google ScholarDigital Library
- A. Saad. Java-based Functionality and Data Management in the automobile|Prototyping at BMW Car IT GmbH. JavaSPEKTRUM. SIGS Datacom, March 2003.Google Scholar
- SCADE suite. http://www.estereltechnologies. com/products/scade-suite/Google Scholar
- EU project Sensoria (IST-2005-016004). http://www.sensoria-ist.eu/Google Scholar
- SPARK toolset. http://www.praxis-his.com/sparkada/Google Scholar
- Spin model checker. http://www.spinroot.comGoogle Scholar
- UMC model checker. http://fmt.isti.cnr.it/umc/Google Scholar
- Unified Modeling Language. http://www.uml.org/Google Scholar
- Uppaal tool. http://www.uppaal.comGoogle Scholar
- 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. Google ScholarDigital Library
Index Terms
- Formal verification of an automotive scenario in service-oriented computing
Recommendations
A logical verification methodology for service-oriented computing
We introduce a logical verification methodology for checking behavioral properties of service-oriented computing systems. Service properties are described by means of SocL, a branching-time temporal logic that we have specifically designed for ...
Formal verification of ASMs using MDGs
We present a framework for the formal verification of abstract state machine (ASM) designs using the multiway decision graphs (MDG) tool. ASM is a state based language for describing transition systems. MDG provides symbolic representation of transition ...
Coverage metrics for formal verification
In formal verification, we verify that a system is correct with respect to a specification. Even when the system is proven to be correct, there is still a question of how complete the specification is and whether it really covers all the behaviors of ...
Comments