Abstract
Methods are needed to help using formal specifications in a practical way. We herein present a method for the development of mixed systems, i.e. systems with both a static and a dynamic part. Our method helps the specifier providing means to structure the system in terms of communicating subcomponents and to give the sequential components using a semi-automatic concurrent automata generation with associated algebraic data types. These components and the whole system may be verified using common set of tools for transition systems or algebraic specifications. Furthermore, our method is equipped with object oriented code generation in Java, to be used for prototyping concerns. In this paper, we present our method on a small example: a transit node component in a communication network.
Chapter PDF
Similar content being viewed by others
References
Luis A. Àlvarez, Juan M. Murillo, Fernando Sánchez, and Juan Hernández. ActiveJava, un modelo de programación concurrente orientado a objeto. In III Jornadas de Ingenería del Software, Murcia, Spain, 1998.
Pascal André. Méthodes formelles et à objets pour le développement du logiciel: Etudes et propositions. PhD Thesis, Université de Rennes I (Institut de Recherche en Informatique de Nantes), Juillet 1995.
Pascal André and Jean-Claude Royer. How To Easily Extract an Abstract Data Type From a Dynamic Description. Research Report 159, Institut de Recherche en Informatique de Nantes, September 1997.
Pascal André, Dan Chiorean, and Jean-Claude Royer. The formal class model. In Joint Modular Languages Conference, pages 59–78, Ulm, Germany, 1994. GI, SIG and BCS.
M. Bidoit, C. Choppy, and F. Voisin. Validation d’une spécification algébrique du “Transit-node” par prototypage et démonstration de théorèmes. Chapitre du Rapport final de l’Opération VTT, Validation et vérification de propriétés Temporelles et de Types de données (commune aux PRC PAOIA et C3), LaBRI, Bordeaux, 1994.
Michel Bidoit. Types abstraits algébriques: spécifications structurées et présentations gracieuses. In Colloque AFCET, Les mathématiques de l’informatique, pages 347–357, Mars 1982.
Tommaso Bolognesi and Ed Brinksma. Introduction to the ISO Specification Language LOTOS. Computer Networks and ISDN Systems, 14(1):25–29, January 1988.
D. Caromel and J. Vayssi_ere. A Java Framework for Seamless Sequential, Multithreaded, and Distributed Programming. In ACM Workshop “Java for High-Performance Network Computing”, pages 141–150, Stanford University, Palo Alto, California, 1998.
Eva Coscia and Gianna Reggio. JTN: A Java-Targeted Graphic Formal Notation for Reactive and Concurrent Systems. In Jean-Pierre Finance, editor, Fundamental Approaches to Software Engineering (FASE’99), volume 1577 of Lecture Notes in Computer Science, pages 77–97. Springer-Verlag, 1999.
Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite Systems, volume B of Handbook of Theoretical Computer Science, chapter 6, pages 243–320. Elsevier, 1990. Jan Van Leeuwen, Editor.
Jan Ellsberger, Dieter Hogrefe, and Amardeo Sarma. SDL: Formal Object-oriented Language for Communicating Systems. Prentice-Hall, 1997.
M. Navarro F. Orejas and A. Sanchez. Implementation and behavioural equivalence: a survey. In M. Bidoit and C. Choppy (Eds.), editors, Recent Trends in data Type Specification, volume 655 of Lecture Notes in Computer Science, pages 93–125. Springer-Verlag, August 1993.
Jean-Claude Fernandez, Hubert Garavel, Alain Kerbrat, Radu Mateescu, Laurent Mounier, and Mihaela Sighireanu. CADP: A Protocol Validation and Verification Toolbox. In 8th Conference on Computer-Aided Verification, pages 437–440, New Brunswick, New Jersey, USA, 1996.
S. Garland and J. Guttag. An overview of LP, the Larch Prover. In Proc. of the Third International Conference on Rewriting Techniques and Applications, volume 355 of Lecture Notes in Computer Science, pages 137–151. Springer-Verlag, 1989.
Gosling, Joy, and Steele. The Java Language Specification. Addison Wesley, 1996.
Wolfgang Grieskamp, Maritta Heisel, and Heiko Dürr. Specifying Embedded Systems with Statecharts and Z: An Agenda for Cyclic Software Components. In Egidio Astesiano, editor, FASE’98, volume 1382 of Lecture Notes in Computer Science, pages 88–106. Springer-Verlag, 1998.
Maritta Heisel. Agendas-A Concept to Guide Software Development Activities. In R. N. Horspool, editor, Proceedings Systems Implementation 2000, pages 19–32. Chapman & Hall, 1998.
Maritta Heisel and Nicole Lévy. Using LOTOS Patterns to Characterize Architectural Styles. In Michel Bidoit and Max Dauchet, editors, TAPSOFT’97 (FASE’97), volume 1214 of Lecture Notes in Computer Science, pages 818–832, 1997.
C.A.R. Hoare. Proof of Correctness of Data Representations. Acta Informatica, 1:271–281, 1972.
ISO/IEC. LOTOS: A Formal Description Technique based on the Temporal Ordering of Observational Behaviour. ISO/IEC 8807, International Organization for Standardization, 1989.
Thomas Lambolais, Nicole Lévy, and Jeanine Souquières. Assistance au développement de spécifications de protocoles de communication. In AFADL’97 Approches Formelles dans l’Assistance au Développement de Logiciel, pages 73–84, 1997.
Juan M. Murillo, Juan Hernández, Fernando Sánchez, and Luis A. Álvarez. Coordinated Roles: Promoting Re-usability of Coordinated Active Objects Using Event Notification Protocols. In Paolo Ciancarini and Alexander L. Wolf, editors, Third International Conference, COORDINATION’99, volume 1594 of Lecture Notes in Computer Science, Amsterdam, The Nederlands, April 1999. Springer-Verlag.
M. Papathomas, J. Hern_andez, J. M. Murillo, and F. S_anchez. Inheritance and expressive power in concurrent object-oriented programming. In LMO’97 Langages et Modèles à Objets, pages 45–60, 1997.
Pascal Poizat, Christine Choppy, and Jean-Claude Royer. Un support méthodologique pour la spécification de systèmes “mixtes”. Research Report 180, Institut de Recherche en Informatique de Nantes, Novembre 1998. http://www./papers /rr180.ps.gz in Poizat’s web page.
Pascal Poizat, Christine Choppy, and Jean-Claude Royer. Une nouvelle méthode pour la spécification en LOTOS. Research Report 170, Institut de Recherche en Informatique de Nantes, Février 1998. http://www./papers/rr170.ps.gz in Poizat’s web page.
Pascal Poizat, Christine Choppy, and Jean-Claude Royer. Concurrency and Data Types: A Specification Method. An Example with LOTOS. In J. Fiadeiro, editor, Recent Trends in Algebraic Development Techniques, Selected Papers of the 13th International Workshop on Algebraic Development Techniques WADT’98, volume 1589 of Lecture Notes in Computer Science, pages 276–291, Lisbon, Portugal, 1999. Springer-Verlag.
Pascal Poizat, Christine Choppy, and Jean-Claude Royer. From Informal Requirements to Object Oriented Code using Structured Concurrent Sequential Communicating Automata. Research Report, Institut de Recherche en Informatique de Nantes, 1999.
Graeme Smith. A Fully-Abstract Semantics of Classes for Object-Z. Formal Aspects of Computing, 7(E):3–65, 1995.
Rational Software and al. Unified Modeling Language, Version 1.1. Technical report, Rational Software Corp, http://www.rational.com/uml, September 1997.
The Raise Method Group. The RAISE Development Method. The Practitioner Series. Prentice-Hall, 1995.
K. Turner. Relating architecture and specification. Computer Networks and ISDN Systems, 29(4):437–456, 1997.
Kenneth J. Turner, editor. Using Formal Description Techniques, An introduction to Estelle, Lotos and SDL. Wiley, 1993.
C.A. Vissers, G. Scollo, M Van Sinderen, and E. Brinksma. Specification styles in distributed systems design and verification. Theoretical Computer Science, (89):179–206, 1991.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Poizat, P., Choppy, C., Royer, JC. (1999). From informal requirements to COOP: a concurrent automata approach. In: Wing, J.M., Woodcock, J., Davies, J. (eds) FM’99 — Formal Methods. FM 1999. Lecture Notes in Computer Science, vol 1709. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48118-4_1
Download citation
DOI: https://doi.org/10.1007/3-540-48118-4_1
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66588-5
Online ISBN: 978-3-540-48118-8
eBook Packages: Springer Book Archive