281
views
0
recommends
+1 Recommend
1 collections
    0
    shares
       
      • Record: found
      • Abstract: found
      • Conference Proceedings: found
      Is Open Access

      A Comparison of Formal Real-Time Specication Languages

      proceedings-article

      , , ,

      Proceedings of the BCS-FACS Northern Formal Methods Workshop (NFM)

      Northern Formal Methods

      23-24 September 1996

      Bookmark

            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
            [0001]Department of Computing, University of Bradford

            Bradford, BD7 1DP, UK
            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 (journal page): https://ewic.bcs.org/
            Categories
            Electronic Workshops in Computing

            Comments

            Comment on this article