Abstract
Formal methods in system engineering have been developed with the aim to enhance safety of complex systems. We introduce a grahical formalism supporting requirements capture for real-time systems in an assumption/commitment style. It is inspired by the timing diagrams informally used in hardware design. The Constraint Diagrams defined here are formalized in the interval temporal logic Duration Calculus developed by Hoare, Ravn and Zhou. Thus we combine rigour of formal methods with intuitivity of graphical representations.
This work was partially funded by the Leibniz Programme of the German Research Council (DFG) under grant Ol 98/1-1.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
A.P. Ravn. Design of Embedded Real-Time Computing Systems. Technical report, ID/DTH, Lyngby, Denmark, 1995.
G. Boriello. Formalized Timing Diagrams. In Proc. European Conference on Design Automation. Belgium, 1992.
C. Antoine, B. Le Goff. Timing Diagrams for writing and checking logical and behavioural properties of integrated systems. In P. Prinetti, P.Camurati, editor, Correct Hardware Design Methodologies. Elsevier Science Publishers, 1992.
H. Langmaack, W.-P. de Roever, J. Vytopil (eds.). Formal Techniques in Real-Time and Fault-Tolerant Systems. Springer, 1994.
Jifeng He, C.A.R.Hoare, M. Fränzle, M. Müller-Olm, E.-R. Olderog, M. Schenke, M.R. Hansen, A.P. Ravn, H. Rischel. Provably Correct Systems. In H. Langmaack, W.P. de Roever, Y. Vytopil, editor, Formal Techniques in Real-Time and Fault-Tolerant Systems. Springer, 1994.
J.W. de Bakker, C. Huizing, W.P. de Roever, G Rozenberg (eds.). Real-Time: Theory in Practice. Springer, 1991.
M. Broy. A Functional Rephrasing of the Assumption/Commitment Specification Style. Technical report, TU München, TUM-I9417, 1994.
M. Fujita, H. Fujisawa. Specification, Verification and and Synthesis of Control Circuits with Prepositional Temporal Logic. In J.A. Darringer, F.J. Rammig, editor, Computer Hardware Description Languages and their Applications. IFIP, Elsevier Science Publishers B.V., 1990.
M. Schenke, E.-R. Olderog. Design of Real-Time Systems: Interface between Duration Calculus and Program Specifications. In STRICT'95. Springer, 1995.
M. von der Beeck. A Comparison of Statecharts Variants. In H. Langmaack, W.-P. de Roever, J. Vytopil, editor, Formal Techniques in Real-Time and Fault-Tolerant Systems. Springer, 1994.
R. Schlör, W. Damm. Specification and Verification of System Level Hardware Designs using Timing Diagrams. In Proc. The European Conference on Design Automation. Paris, France, 1993.
Y.S. Ramakrishna, P.M. Melliar-Smith, L.E. Moser, L.K. Dillon, G. Kutty. Really Visual Temporal Reasoning. In Proc. 14th RTSS, Raliegh-Durham. IEEE Press, 1993.
Z. Manna, A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems — Specification. Springer, 1992.
Zhou Chaochen, C.A.R. Hoare, A.P. Ravn. A Calculus of Durations. Information Processing Letters, 40(5), 1991.
Zhou Chaochen, Dang Van Hung, Li Xiaoshan. A Duration Calculus with Infinite Intervals. Technical report, UNU/IIST Report No. 40, 1995.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dietz, C. (1996). Graphical formalization of real-time requirements. In: Jonsson, B., Parrow, J. (eds) Formal Techniques in Real-Time and Fault-Tolerant Systems. FTRTFT 1996. Lecture Notes in Computer Science, vol 1135. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61648-9_51
Download citation
DOI: https://doi.org/10.1007/3-540-61648-9_51
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61648-1
Online ISBN: 978-3-540-70653-3
eBook Packages: Springer Book Archive