Abstract
While designing interactive software, the use of a formal specification technique is of great help by providing non-ambiguous, complete and concise notations. The advantages of using such a formalism is widened if it is provided by formal analysis techniques that allow to prove properties about the design, thus giving an early verification to the designer before the application is actually implemented. This paper presents such a formalism, called Interactive Cooperative Objects. The paper mainly focuses on the formal analysis of the design, describing the calculation of its properties and their interpretation in terms of the software behaviour.
Chapter PDF
Similar content being viewed by others
References
Bastide R. (1992). Cooperative Objects: a formalism for modeling concurrent systems. PhD Dissertation. (In French).
Bastide R., Palanque P. (1990). Petri net with objects for the design, validation and prototyping of user-driven interfaces. In proceedings Interact’90, Elsevier, p. 625–631.
Brauer W. (Editor) (1986). LNCS 254 & 255, Springer Verlag.
Dix A. (1991). Formal methods for interactive systems. Academic Press.
Feldbrudge F., Jensen K. (1986). Petri net tool overview in (Brauer 1986 ).
Harrison M. & Thimbelby H. (eds.) (1990). Formal Methods in HCI. Cambridge University Press.
Palanque P., Bastide R. (1994a). Petri net based Design of User-driven Interfaces Using Interactive Cooperative Object Formalism; In (Paterno 1994).
Palanque P., Bastide R., Senges V. (1994b). Automatic code generation from a high-level Petri net based specification; In proceedings of EWHCI’94.
Palanque P., Bastide R., Sibertin C., Dourte L. (1993). Design of User-Driven Interfaces using Petri nets and Objects, In proceedings of CAISE’93. LNCS 685, Springer-Verlag.
Paterno F. (Editor) (1994). Proceedings of EG Workshop on Design, Specification and Verification of Interactive Systems.
Peterson J.L. (1981). Petri net theory and modeling of systems.Prentice-hall.
Sibertin-blanc C. (1993). A client server protocol for the composition of Petri nets. In proceedings of Application and Theory of Petri nets LNCS 691, Chicago.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1995 IFIP International Federation for Information Processing
About this chapter
Cite this chapter
Palanque, P., Bastide, R. (1995). Verification of an Interactive Software by Analysis of its Formal Specification. In: Nordby, K., Helmersen, P., Gilmore, D.J., Arnesen, S.A. (eds) Human—Computer Interaction. IFIP Advances in Information and Communication Technology. Springer, Boston, MA. https://doi.org/10.1007/978-1-5041-2896-4_32
Download citation
DOI: https://doi.org/10.1007/978-1-5041-2896-4_32
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-5041-2898-8
Online ISBN: 978-1-5041-2896-4
eBook Packages: Springer Book Archive