Abstract
The purpose of this paper is to demonstrate how transformation can be used to derive a high integrity implementation of a train controller from an algorithmic specification. The paper begins with a general discussion of high consequence systems (e.g., software systems) and describes how rewrite-based transformation systems can be used in the development of such systems. We then discuss how such transformations can be used to derive a high assurance controller for the Bay Area Rapid Transit (BART) system from an algorithmic specification.
This work was supported by the United States Department of Energy under Contract DE-AC04–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
Ricky W. Butler and George B. Finelli.The Infeasibility of Quantifying the Reliability of Life-Critical Real-Time Software.
C. Michael Holloway.Why Engineers Should Consider Formal Methods. J. of Computer and Mathematics with Applications,29, 2, 1995, 91–114.
Proc.Intl. Conf on Automated Deduction, CADE-13, New Jersey, July 1996, 538–552.
Deepak Kapur and Victor Winter.On the Construction of a Domain Language for a Class of Reactive Systems. Proceedings of the High Integrity Software (HIS) Conference, Nov. 1999.
arithmetic circuits,” to appear inJ. of Software Tools for Technology Transfer, Springer Verlag, 2000.
Robert P. Kurshan.Computer-Aided Verification of Coordinating Processes. Princeton Series in Computer Science, 1994.
C. Lewerentz and T. Lindner.Formal Development of Reactive Systems: Case Study Production Cell. Lecture Notes in Computer Science Vol. 891, Springer-Verlag.
Carroll Morgan.Programming from Specifications. Prentice Hall International Series in Computer Science, 1990.
H. Partsch and R. Steinbruggen.Program Transformation Systems. ACM Computing Surveys, Vol. 15, No. 3, pp 199–236, Sept 1983.
John Rushby.Formal Methods and their Role in the Certification of Critical Systems.
S. Stepney.High Integrity Compilation: A Case Study. Prentice Hall, 1993.
M. Ward.Specifications and Programs in the Wide Spectrum Language. Durham University, Technical Report, Durham, 1991.
V. L. Winter.An Overview of HATS: A Language Independent High Assurance Transformation System. Proceedings of the IEEE Symposium on Application-Specific Systems and Software Engineering Technology (ASSET), March 24–27, 1999.
Bay Area Rapid Transit District Advance Automated Train Control System Case Study Description. Proceedings of the High Integrity Software (HIS) Conference, Nov. 1999.
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
Winter, V.L., Kapur, D., Berg, R.S. (2001). A Refinement-Based Approach to Deriving Train Controllers. 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_9
Download citation
DOI: https://doi.org/10.1007/978-1-4615-1391-9_9
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4613-5530-4
Online ISBN: 978-1-4615-1391-9
eBook Packages: Springer Book Archive