Coalgebraic semantics for component systems
Proceedings of the 2004 international conference on Architecting Systems with Trustworthy Components
Pages 245 - 261
Abstract
We propose a novel approach for defining the semantics of component systems coinductively. In particular, we formalize a framework for component systems within the theorem prover Isabelle/HOL. Using this formalization, we are able to formally reason about and verify aspects of component composition and interaction. Furthermore, we discuss strategies for adaptor code generation from a given component system specification. We demonstrate the applicability of our approach by a case study.
References
[1]
Jean-Raymond Abrial. The B-Book, 1996.
[2]
Manfred Broy, Frank Dederich, Claus Dendorfer, Max Fuchs, Thomas Gritzner, and Rainer Weber. The Design of Distributed Systems - An Introduction to FOCUS. Technical Report TUM-I9202, Technische Univerität München, 1992.
[3]
Jan Olaf Blech, Sabine Glesner, and Johannes Leitner. Formal Verification of Java Code Generation from UML Models. In Proceedings of the 3rd International Fujaba Days 2005: MDD in Practice. Technical Report, University of Paderborn, September 2005.
[4]
Jan A. Bergstra, Alban Ponse, and Scott A. Smolka, editors. Handbook of Process Algebra. Elsevier, 2001.
[5]
E.M. Clarke, O. Grumberg, and D. Long. Verification Tools for Finite-State Concurrent Systems. In J.W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, A Decade of Concurrency - Reflections and Perspectives, pages 124-175. Springer, Lecture Notes in Computer Science, Vol. 803, 1993.
[6]
Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. Model Checking. The MIT Press, 1999.
[7]
Erich Gamma, Richard Helm, Ralph Johnson, and John Vlissides. Design patterns: elements of reusable object-oriented software. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA, 1995.
[8]
Dirk Heuzeroth. Aspektorientierte Konfiguration und Adaption von Komponenteninteraktionen. PhD thesis, Universität Karlsruhe, 2004.
[9]
Ulrich Hensel, Marieke Huisman, Bart Jacobs, and Hendrik Tews. Reasoning about Classes in Object-Oriented Languages: Logical Models and Tools. In Chris Hankin, editor, Programming Languages and Systems - ESOP'98, 7th European Symposium on Programming, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS'98, pages 105-121, Lisbon, Portugal, 1998. Springer Verlag, Lecture Notes in Computer Science, Vol. 1381.
[10]
C.A.R. Hoare. Communicating Sequential Processes. Prentice Hall International, 1985.
[11]
Marieke Huisman. Reasoning about Java programs in higher order logic using PVS and Isabelle. PhD thesis, Faculty of Science, University of Nijmegen, 2001.
[12]
Bart Jacobs and Jan Rutten. A Tutorial on (Co)Algebras and (Co)Induction. EATCS Bulletin, 67:222-259, 1997.
[13]
Robin Milner. Communicating and Mobile Systems: the pi-Calculus. Cambridge University Press, 1999.
[14]
Lawrence C. Paulson. A Fixedpoint Approach to (Co)Inductive and (Co)Datatype Definitions, 2004. available at www.cl.cam.ac.uk/ Research/HVG/Isabelle/dist/Isabelle2004/doc/ind-defs.pdf.
[15]
Roberto Passerone, Luca de Alfaro, Thomas A. Henzinger, and Alberto L. Sangiovanni-Vincentelli. Convertibility verification and converter synthesis: two faces of the same coin. In ICCAD '02: Proceedings of the 2002 IEEE/ACM international conference on Computer-aided design, pages 132-139, New York, NY, USA, 2002. ACM Press.
[16]
Christine Röckl. On the Mechanized Validation of Infinite-State and Parameterized Reactive and Mobile Systems. PhD thesis, Technische Universität München, 2001.
[17]
Haykal Tej and Burkhart Wolff. A Corrected Failure Divergence Model for CSP in Isabelle/HOL. In FME '97: Proceedings of the 4th International Symposium of Formal Methods Europe on Industrial Applications and Strengthened Foundations of Formal Methods, pages 318-337, London, UK, 1997. Springer-Verlag.
[18]
Andrzej Wasowski. On efficient program synthesis from statecharts. In LCTES '03: Proceedings of the 2003 ACM SIGPLAN conference on Language, compiler, and tool for embedded systems, pages 163-170, New York, NY, USA, 2003. ACM Press.
[19]
A. Zündorf. Rigorous Object Oriented Software Development with Fujaba. Unpublished draft, 2002.
Recommendations
Coinductive Verification of Program Optimizations Using Similarity Relations
Formal verification methods have gained increased importance due to their ability to guarantee system correctness and improve reliability. Nevertheless, the question how proofs are to be formalized in theorem provers is far from being trivial, yet very ...
Coinductive big-step operational semantics
Using a call-by-value functional language as an example, this article illustrates the use of coinductive definitions and proofs in big-step operational semantics, enabling it to describe diverging evaluations in addition to terminating evaluations. We ...
Higher-Order Separation Logic in Isabelle/HOLCF
We formalize higher-order separation logic for a first-order imperative language with procedures and local variables in Isabelle/HOLCF. The assertion language is modeled in such a way that one may use any theory defined in Isabelle/HOLCF to construct ...
Comments
Information & Contributors
Information
Published In
December 2004
298 pages
ISBN:3540358005
Publisher
Springer-Verlag
Berlin, Heidelberg
Publication History
Published: 12 December 2004
Author Tags
Qualifiers
- Article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 25 Oct 2024
Other Metrics
Citations
View Options
View options
Get Access
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in