Abstract
Temporal Language of Transitions (TLT) is a framework for the design and verification of distributed systems being developed at Siemens. It consists of formalisms to model systems and specify their properties as well as methods like refinement and composition. In this paper we introduce TLT and focus on the integration of efficient verification techniques like model checking. This is especially important in an industrial environment. Using a lift control program as example, we introduce the TLT programming language and the TLT logic, calculus, and proof techniques. We also report on the performance of model checking.
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. Computer-Aided Verification of Concurrent Systems. PhD thesis, Faculty of Informatics, Technical University of Munich, D-80290 Munich, Germany, In preparation 1995.
J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98:142–170, 1992.
Randal E. Bryant. Symbolic boolean manipulation with ordered binarydecision diagrams. ACM Computing Surveys, 24(3):293–318, September 1992.
Jorge Cuéllar and Dieter Barnard. A Tutorial Introduction to TLT. Part I: The Design of Distributed Systems. Technical report, ZFE BT SE 11, Corporate Research and Development, Siemens AG, D-81730 Munich, 1994.
Jorge Cuéllar, Dieter Barnard, and Martin Huber. A Tutorial Introduction to TLT. Part II: The Verification of Distributed Systems. Technical report, ZFE BT SE 11, Corporate Research and Development, Siemens AG, D-81730 Munich, 1994.
Jorge Cuéllar and Gerd Gouverneur. Synthese und Verifikation paralleler Systeme am Beispiel einer verteilten Zugsteuerung. Technical report, Siemens AG, ZFE BT SE 11, D-81730 München, Germany, 1992.
Jorge Cuéllar and Gerd Gouverneur. Eine Einführung in TLT. Technical report, Siemens ZFE BT SE 11, D-81730 München, Germany, 1994.
K. Mani Chandy and Jayadev Misra. Parallel Program Design — A Foundation. Addison-Wesley, Reading, Massachusetts, 1988.
Jorge Cuéllar and Isolde Wildgruber. An Introduction to TLT Illustrated on a Lift Control Program. Technical report, ZFE BT SE 11, Corporate Research and Development, Siemens AG, D-81730 Munich, 1994.
Gerd Gouverneur. Temporal Logic of Transitions. PhD thesis, Fakultät für Informatik, Universität Kaiserslautern, Kaiserslautern, Germany, To appear 1995.
G.E. Hughes and M.J. Cresswell. An Introduction to Modal Logic. Methuen and Co, London, 1972.
Leslie Lamport. The Temporal Logic of Actions. Technical Report 79, Digital Systems Research Center, Palo Alto, California, December 1991.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cuéllar, J., Wildgruber, I., Barnard, D. (1994). Combining the design of industrial systems with effective verification techniques. In: Naftalin, M., Denvir, T., Bertran, M. (eds) FME '94: Industrial Benefit of Formal Methods. FME 1994. Lecture Notes in Computer Science, vol 873. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58555-9_120
Download citation
DOI: https://doi.org/10.1007/3-540-58555-9_120
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58555-8
Online ISBN: 978-3-540-49031-9
eBook Packages: Springer Book Archive