Abstract
This paper presents the TLT specification of the steam-boiler control-program described in Chapter AS. The text of the TLT specification of the control program is short and easily understandable. Due to the chosen abstraction level, the proofs that it satisfies the specification of Chapter AS are very simple. TLT has the advantage that the algorithm may be directly described as performing macro-steps. A macro step is specified not as a sequence of micro-steps but rather as a set of constraints (which may be formulated in first-order logic). These constraints relate the current state of the controller (i.e. the information that the controller has about the environment), the current input and the corresponding reaction (and change of state) of the controller. (Of course, the macro-step is implemented as a sequence of micro-steps). Thus, to argue about the program we may rely more heavily on prepositional or first-order logic rather than on temporal logic.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Dieter Barnard and Simon Crosby. The Specification and Verification of an ATM Signalling Protocol. In Proc. of 15th IFIP PSTV'95, Warsaw, June 1995.
H. Busch. A Practical Method for Reasoning About Distributed Systems in a Theorem Prover. In Higher Order Logic Theorem Proving and its Applications — 8th International Workshop, Aspen Grove, UT, USA, Proceedings, pages 106–121. Springer-Verlag, LNCS 971, September 1995.
Jorge Cuéllar, Dieter Barnard, and Martin Huber. A Solution relying on the Model Checking of Boolean Transition Systems. In The RPC-Memory Specification Problem, to appear in LNCS, 1996.
Jorge Cuéllar, Dieter Barnard, and Martin Huber. Rapid Protyping for an Assertional Specification Language. TACAS'96, LNCS 1055, March 1996.
C. Courcoubetis, S. Graf, and J. Sifakis. An Algebra of Boolean Processes. In Proc. of CAV'91, pages 454–465, 1991.
Jorge Cuéllar and Martin Huber. The FZI Production Cell Case Study: A distributed solution using TLT. In Formal Development of Reactive Systems: Case Study Production Cell, volume 891 of LNCS. Springer-Verlag, 1995.
J. R. Cuéllar, I. Wildgruber, and D. Barnard. Combining the Design of Industrial Systems with Effective Verification Techniques. In M. Naftalin, T. Denvir, and M. Betran, editors, Proc. of FME'94, volume 873 of LNCS, pages 639–658, Barcelona, Spain, October 1994. Springer-Verlag.
T. Filkorn, H.A. Schneider, A. Scholz, A. Strasser, and P. Warkentin. SVE User's Guide. Technical report, Siemens AG, ZFE T SE 1, D-81730 München, Germany, 1994.
R.P. Kurshan. Computer Aided Verification of Coordinating Processes. Princeton University Press, 1994.
L. Lamport. The Temporal Logic of Actions. ACM Transactions on Programming Languages and Systems, 16(3):872–923, May 1994.
Author information
Authors and Affiliations
Corresponding author
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Cuéllar, J., Wildgruber, I. (1996). The steam-boiler problem — A TLT solution. 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/BFb0027236
Download citation
DOI: https://doi.org/10.1007/BFb0027236
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