Abstract
A key step in the construction of high consequence software is its specification in a formal framework. In order to minimize the difficulty and potential for error, a specification should be expressed in a domain language supporting operators and structures that are intrinsic to the class of algorithms one wishes to specify.
In this paper we describe a language that is suitable for the algorithmic specification of software controllers for a class of reactive systems of which the Bay Area Rapid Transit (BART) system is an instance. We then specify an abstract controller for a subset of BART using this language.
This work was supported by the United States Department of Energy under Contract DE-AC0–94AL85000. Sandia is a multiprogram laboratory operated by Sandia Corporation, a Lockheed Martin Company for the United States Department of Energy
Deepak Kapur was also partially supported by NSF grant nos. CCR-9996150 and CDA-9503064
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
K. A. Ghosh, B. W. Johnson, and J. A. Profeta, III. A Distributed Safety-Critical System for Real-Time Train Control. Proceedings of the 21st Annual Conference of the IEEE Industrial Electronics Society (IECON ‘95), Orlando, Florida, November 6–10, 1995, pp. 760–767.
H. Gomaa. Software Design Methods for Concurrent and Real-Time Systems. Addison Wesley, 1993.
B. Johnson and J. H. Aylor. Reliability and Safey Analysis of a Fault-Tolerant Controller. IEEE Transactions on Reliability, Vol. R-35, No. 4, October 1986, pp. 355–362.
D. Kapur and M. Subramaniam. “Using an induction prover for verifying arithmetic circuits,” to appear in J. of Software Tools for Technology Transfer, Springer Verlag, 2000.
D. Kapur, and H. Zhang. “An overview of Rewrite Rule Laboratory (RRL),” J. of Computer and Mathematics with Applications, 29, 2, 1995, 91–114.
C. Lewerentz and T. Lindner. Formal Development of Reactive Systems: Case Study Production Cell. Lecture Notes in Computer Science Vol. 891, Springer-Verlag.
Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, 1995.
R. Janicki, D. Parnas, and J. Zucker. Tabular Representations in Relational Documents. CRL Report No. 313, November 1995.
Victor Winter, Deepak Kapur, and Raymond Berg. A Refinement-based Approach to Deriving Train Controllers. High Integrity Software, Kluwer (eds. Winter and Bhattacharya), 2000.
Victor Winter, Raymond Berg, and Jim Ringland. Bay Area Rapid Transit District Advance Automated Train Control System Case Study Description
H. Zhang, D. Kapur, and M.S. Krishnamoorthy, “A mechanizable induction principle for equational specifications,” Proc. 9th Intl. Conf. Automated Deduction (CADE), Springer LNCS 310, (eds. Lusk and Overbeek), 1988, 250–265.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer Science+Business Media New York
About this chapter
Cite this chapter
Kapur, D., Winter, V.L. (2001). On the Construction of a Domain Language for a Class of Reactive Systems. In: Winter, V.L., Bhattacharya, S. (eds) High Integrity Software. The Kluwer International Series in Engineering and Computer Science, vol 577. Springer, Boston, MA. https://doi.org/10.1007/978-1-4615-1391-9_8
Download citation
DOI: https://doi.org/10.1007/978-1-4615-1391-9_8
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4613-5530-4
Online ISBN: 978-1-4615-1391-9
eBook Packages: Springer Book Archive