Abstract
This paper concentrates on the specification of the requirements for the Steam-Boiler Control System. It contains a detailed analysis and specification of the sent and received messages, the different states the system can be in, etc. Special emphasis is put on the analysis of checking the physical devices and detecting failures in the system environment.
The paper uses an original approach that combines algebraic specification techniques with a notion of implicit state. State changes are achieved by so-called modifiers.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Bidoit, M., Gaudel, M-C. and Mauboussin, A., How to make algebraic specifications more understandable? An experiment with the PLUSS specification language. Science of Computer Programming, vol. 12, nℴ 1, pp. 1–38, June 1989.
Bauer J.C., Generic Problem Competition, a component of the International Symposium Design and Review of Software Controlled Safety-Related Systems, Institute for Risk Research, University of Waterloo, 1992.
Bidoit M., PLUSS, un langage pour le développement de spécifications algébriques modulaires, Thèse d'Etat, Université de Paris-Sud, Orsay, May 1989.
Craigen D., Gerhart S., Ralston T., On the use of formal methods in industry — an authoritative assessment of the efficacy, utility, and applicability of formal methods to systems design and engineering by the analysis of real industrial cases, Report to the US National Institute of Standards and Technology, March 1993.
Expériences de spécification formelle d'un pilote automatique de métro. Thèse, Université de Paris-Sud, 1992.
Dauchy P., Gaudel M.-C., Algebraic Specifications with Implicit State, Rapport LRI nℴ887, Feb. 1994.
Dauchy P., Gaudel M-C., Marre B., Using Algebraic Specifications in Software Testing: a case study on the software of an automatic subway, Journal of Systems and Software, vol. 21, nℴ 3, June 1993, pp. 229–244.
Dauchy P., Marre B., Test data selection from algebraic specifications: application to an automatic subway module, 3rd European Software Engineering Conference, (ESEC'91), Milan, 1991, LNCS nℴ 550.
Ehrig H., Orejas F., Dynamic Abstract Data Types: an informal proposal, EATCS bulletin, Sept. 1994.
Gaudel M.-C., Génération et Preuve de Compilateurs basées sur une Sémantique Formelle des Langages de Programmation, Thèse d'état, INPL (Nancy), 1980.
Gaudel M.-C., Correctness Proofs of Programming Language Translations, IFIP-TC2 Working Conference on Formal Description of Programming Concepts, Garmisch-Partenkirchen, June 83, North-Holland 1983, pp. 25–43.
Gaudel M-C., Structuring and Modularizing Algebraic Specifications: the PLUSS specification language, evolutions and perspectives, STACS'92, Cachan, Feb. 1992, LNCS nℴ577, pp. 3–18, Springer-Verlag.
Lévy N., Definition of “add-a-component”, a Specification Construction Process Operator, Technical Report ForSem-005-R, ICARUS ESPRIT Project, 1990.
Souquières J., Lévy N., Description of Specification Developments, 1st IEEE Symposium on Requirements Engineering, San Diego, January 1993.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Gaudel, MC., Dauchy, P., Khoury, C. (1996). A formal specification of the Steam-Boiler Control problem by algebraic specifications with implicit state. In: Abrial, JR., Börger, E., Langmaack, H. (eds) Formal Methods for Industrial Applications. Lecture Notes in Computer Science, vol 1165. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0027240
Download citation
DOI: https://doi.org/10.1007/BFb0027240
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61929-1
Online ISBN: 978-3-540-49566-6
eBook Packages: Springer Book Archive