Skip to main content

Systematic Validation of a Relational Control Program for the Bay Area Rapid Transit System

  • Chapter
High Integrity Software

Part of the book series: The Kluwer International Series in Engineering and Computer Science ((SECS,volume 577))

Abstract

The failure of safety-critical systems, such as aircraft control systems, railway control systems, and nuclear power plant control systems, can cause catastrophic losses of life and property. Hence, it is imperative to assure the reliability and safety of these systems to a very high degree of confidence.

It is infeasible to perform this type of ultrahigh reliability analysis by treating the entire system as one unit. This paper develops an approach that combines relational programs with iterative enhancement. It allows a complex system to be divided into a series of increments such that each increment is decomposed into subsystems that can be independently assessed. An increment is related to the previous increment via transformations or clearly delineated enhancements that can be assessed independently. The subsystems are then automatically composed together to obtain the system.

The approach guarantees that the reliability and safety of the system can be inferred from the corresponding properties of the individual subsystems. It is illustrated using a case study drawn from the Bay Area Rapid Transit system project.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 129.00
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 169.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 169.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  • C. Atkinson.Object-Oriented Reuse, Concurrency and Distribution. Addison-Wesley&ACM Press, New York, NY, 1991.

    MATH  Google Scholar 

  • Farokh B. Bastani. Relational Programs: Architecture for Robust Process-Control Programs. To appear in —emphAnnals of Software Engineering.

    Google Scholar 

  • F.B. Bastani, V.L. Winter, and I.-L. Yen. Dependability of relational programs. InProc. Of the 1999 IEEE Intl. Symp. On Software Reliability Engineering, Boca Raton, FL, Nov. 1999.

    Google Scholar 

  • D. Coleman, F. Hayes, and S. Bear. Introducing Objectcharts or How to use Statecharts in object-oriented design,”IEEE Trans, on Softw. Eng., 18(1):9–18, Jan. 1992.

    Article  Google Scholar 

  • D. Harel. Statecharts: A visual formalism for complex systems.Sci. of Comput Prog., Vol. 8, 1987, pp. 231–274.

    Article  MathSciNet  MATH  Google Scholar 

  • D. Harel, H. Lachover, A. Naamad, A. Pnueli, M. Politi, R. Sherman, A. Shtull-Trauring, and M. Trakhtenbrot. Statemate: A working environment for the development of complex reactive systems.IEEE Trans. on Softw. Eng., 16(4):403–414, Apr. 1990.

    Article  Google Scholar 

  • D. Jackson. Structuring Z specifications with views.ACM trans. Softw. Eng. and Meth., 4(4):365–389, Oct. 1995.

    Article  Google Scholar 

  • C.B. Jones. Tentative steps towards a development method for interfering programs.ACM Trans. Prog. Lang, ad Sys., 5(4):596–619, Oct. 1983.

    Article  MATH  Google Scholar 

  • G. Kiczales, J. Lamping, A. Mendhekar, C. Maeda, C.V. Lopes, J.-M. Loigtier, and J. Irwin. Aspect-Oriented Programming.Prof. European Cong, on Object-Oriented Programming (ECOOP), Finland, June 1997.

    Google Scholar 

  • S.S. Lam and A.U. Shankar. A theory of interfaces and modules: I — Composition Theorem.IEEE Trans, on Softw. Eng., 20(1):55–71, Jan. 1994.

    Article  Google Scholar 

  • N.G. Leveson, M.P.E. Heimdahl, H. Hildreth, and J.D. Reese. Requirements specification for process-control systems.IEEE Trans, on Softw. Eng., 20(9):684–707, Sep. 1994.

    Article  Google Scholar 

  • Reasoning, Inc., Code-Base Management System (CBMS), Mountain View, CA,1997.

    Google Scholar 

  • V.L. Winter and J.M. Boyle. Proving refinement transformations for deriving high-assurance software. InProceedings of the IEEE High-Assurance Systems Engineering Workshop, Oct. 1996.

    Google Scholar 

  • V.L. Winter, Private communication, July 1998.

    Google Scholar 

  • Victor Winter, Raymond Berg and Jim Ringland. “Bay Area Rapid Transit District Advanced automated Train Control System Case Study Description”, 1999.

    Google Scholar 

  • P. Zave. A distributed alternative to Finite-State-Machine specifications.ACM Trans, on Prog. Lang, and Sys., 7(l):10–36, Jan. 1985.

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2001 Springer Science+Business Media New York

About this chapter

Cite this chapter

Bastani, F.B., Reddy, V., Srigiriraju, P., Yen, IL. (2001). Systematic Validation of a Relational Control Program for the Bay Area Rapid Transit System. 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_10

Download citation

  • DOI: https://doi.org/10.1007/978-1-4615-1391-9_10

  • Publisher Name: Springer, Boston, MA

  • Print ISBN: 978-1-4613-5530-4

  • Online ISBN: 978-1-4615-1391-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics