- Record: found
- Abstract: found
- Conference Proceedings: found
A Comparison of Formal Real-Time Specication Languages
proceedings-article
A.S. Evans , D.R.W. Holton , L.M. Lai , P. Watson
September 1996
Proceedings of the BCS-FACS Northern Formal Methods Workshop (NFM)
Northern Formal Methods
23-24 September 1996
Abstract
In this paper we compare four languages for real time systems specification, namely Timed Z, Timed CSP, Timed CCS and TE-LOTOS, by applying them to the benchmark Railroad Crossing problem. We use slightly different sets of assumptions in each of our solutions in order to investigate how the presence or absence of such assumptions affects the resulting solution. We pay particular attention to the level of justification we may ascribe to each assumption; it may be explicit or implicit in the problem statement, implicit in our knowledge of real- world railroad crossings, or none of these, in which case it must be regarded as a simplifying assumption. We compare and evaluate the resulting specifications in each of the four languages. Our solution in Timed Z is shown to be on a different level to the three process algebras, being much more abstract, closer to the English specification and further from an implementation. It is argued that the three process algebras have essentially equivalent expressive power over the domain of this problem. We compare the proofs in each of the process algebra formalisms. Timed CSP has a well developed dedicated formal proof system, while the proof methods required by Timed CCS and TE-LOTOS are much more ad hoc. In these two cases we use proof techniques based on path and state analysis. We briefly evaluate the Railroad Crossing case study itself. It is found to be a problem of great generality with hidden subtleties; we argue that this problem can teach us much about how to approach real-time specification tasks, and therefore must be considered a highly successful benchmark problem.
Content
Author and article information
Conference
September
1996
September
1996
: 1-21
Affiliations
Article
10.14236/ewic/FA1996.7
f0f963a1-d6f7-492c-ab29-739aac4f2980
© A.S. Evans et al. Published by BCS Learning and Development Ltd. Proceedings of
the BCS-FACS Northern Formal Methods Workshop, Ilkley, UK
This work is licensed under a Creative Commons Attribution 4.0 Unported License. To view a copy of this license, visit http://creativecommons.org/licenses/by/4.0/
Proceedings of the BCS-FACS Northern Formal Methods Workshop
NFM
Ilkley, UK
23-24 September 1996
Electronic Workshops in Computing (eWiC)
Northern Formal Methods
Product
Product Information: 1477-9358BCS Learning & Development
Self URI (article page):
https://www.scienceopen.com/hosted-document?doi=10.14236/ewic/FA1996.7
Self URI (journal page):
https://ewic.bcs.org/
Categories
Electronic Workshops in Computing