Abstract
Since its introduction in 1978, the SCR (Software Cost Reduction) tabular notation has been used to represent the requirements of numerous safety-critical systems, including avionics systems, space systems, and control systems for nuclear plants. Our group has formulated a state-machine semantics for the SCR notation and a set of software tools for analyzing requirements specifications in the SCR tabular notation. To demonstrate the benefits of the SCR method for developing safety-critical systems, this chapter describes the application of SCR to a complex portion of the Advanced Automated Train Control (AATC) system under development for the Bay Area Rapid Transit (BART) system. Examples from an SCR specification of the required behavior of the AATC system are provided. The positive impact of applying our approach to the construction of the AATC system is summarized, and some important issues raised during the case study are discussed.
This work is funded by the Office of Naval Research.
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.
Similar content being viewed by others
References
T. A. Alspaugh, S. R. Faulk, K. H. Britton, R. A. Parker, D. L. Parnas, and J. E. Shore. Software Requirements for the A-7E Aircraft. Technical Report NRL-9194, Naval Research Lab., Wash., DC, 1992.
M. Archer, C. Heitmeyer, and S. Sims. TAME: A PVS Interface To Simplify Proofs for Automata Models. In Proc. User Interfaces for Theorem Provers, Eindhoven, Netherlands, July 1998. Eindhoven University of Technology. Eindhoven University Technical Report.
R. Bharadwaj and C. Heitmeyer. Model Checking Complete Requirements Specifications using abstraction. Automated Software Engineering Journal, 6(1), January 1999.
R. Bharadwaj and C. Heitmeyer. Hardware/Software Co-Design and Co-Validation Using the SCR Method. In Proceedings of the IEEE International High Level Design Validation and Test Workshop (HLDVT’99), San Diego, CA, November 1999.
R. Bharadwaj and S. Sims. Salsa: Combining Constraint Solvers with BDDs for Automatic Invariant Checking. In Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS ‘2000), Berlin, March 2000.
E. M. Clarke and J. M. Wing. Formal methods: State of the art and future directions. A CM Computing Surveys, 28(4):626–643, December 1996.
Judy Crow, Sam Owre, John Rushby, Natarajan Shankar, and Mandayam Srivas. A Tutorial Introduction to PVS. Technical report, Computer Science Lab, SRI Int’l, Menlo Park, CA, April 1995. (Presented at WIFT’95: Workshop on Industrial-Strength Formal Specification Techniques, Boca Raton, FL).
Steve Easterbrook and John Callahan. Formal methods for verification and validation of partial specifications: A case study. Journal of Systems and Software, 1997.
Stuart R. Faulk, Lisa Finneran, James Kirby, Jr., S. Shah, and J. Sutton. Experience applying the CoRE Method to the Lockheed C-130J. In Proc. 9th Annual Conf. on Computer Assurance (COMPASS ‘94), pages 3–8, Gaithersburg, MD, June 1994.
A. Gargantini and C. Heitmeyer. Automatic Generation of Tests from Requirements Specifications. In Proc. ACM 7th Eur. Software Eng. Conf. and 7th ACM SIGSOFT Symp. on the Foundations of Software Eng. (ESEC/FSE99), Toulouse, FR, September 1999.
C. L. Heitmeyer, R. D. Jeffords, and B. G. Labaw. Automated Consistency Checking of Requirements Specifications. A CM Transactions on Software Engineering and Methodology, 5(3):231–261, April-June 1996.
Constance L. Heitmeyer, Ralph D. Jeffords, and Bruce G. Labaw. Tools for Analyzing SCR-Style Requirements Specifications: A Formal Foundation. Technical report, Naval Research Lab., Wash., DC, 1998. Draft.
Constance Heitmeyer, James Kirby, Jr., Bruce Labaw, and Ramesh Bharad-waj. SCR*: A Toolset for Specifying and Analyzing Software Requirements. In Moshe Vardi and Alan Hu, editors, Proc. Computer-Aided Verification, 10th Annual Int’l Conf. (CAV’98), (LNCS U27), pages 526–531, Vancouver, Canada, June/July, 1998.
C. Heitmeyer, J. Kirby, B. Labaw, M. Archer, and R. Bharadwaj. Using Abstraction and Model Checking to Detect Safety Violations in Requirements Specifications. IEEE Trans, on Softw. Eng., 24(11), November 1998.
C. L. Heitmeyer and John McLean. Abstract Requirements Specifications: A New Approach and Its Application. IEEE Trans. Softw. Eng., SE-9(5):580–589, September 1983.
Kathryn L. Heninger. Specifying software requirements for complex systems: New techniques and their application. IEEE Trans. Softw. Eng., SE-6(1):2–13, Jan 1980.
K. Heninger, D. L. Parnas, J. E. Shore, and J. W. Kallander. Software Requirements for the A-7E Aircraft. Technical Report 3876, Naval Research Lab., Wash., DC, 1978.
G. J. Holzmann. The Model Checker SPIN. IEEE Transactions on Software Engineering, 23(5):279–295, May 1997.
Ralph Jeffords and Constance Heitmeyer. Automatic Generation of State Invariants from Requirements Specifications. In Proc. ACM SIGSOFT Sixth Int’l Symp. on the Foundations of Softw. Eng. (FSE-6), pages 56–69, Lake Buena Vista, FL, November 1998. ACM.
J. Kirby, M. Archer and C. Heitmeyer. Applying formal methods to an information security device: an experience report. In Proc. 4th IEEE Intern. Symp. on High Assurance Systems Eng. (HASE99), November 1999.
R. Kurshan. Formal verification in a commercial setting. In Proc., Design Automation Conference, June 1997.
Steve Miller. Specifying the mode logic of a flight guidance system in CoRE and SCR. In Proc. 2nd ACM Workshop on Formal Methods in Software Practice (FMSP’98), March 1998.
NASA. Formal Methods Specification and Verification Guidebook for Software and Computer Systems, Vol. I: Planning and Technology Insertion. Technical report NASA/TP-98–208193, NASA, Washington, DC, December 1998.
David L. Parnas, G. J. K. Asmis, and Jan Madey. Assessment of Safety-Critical Software in Nuclear Power Plants. Nuclear Safety, 32(2): 189–198, April-June 1991.
David L. Parnas and Paul C. Clements. A Rational Design Process: How and Why to Fake It. IEEE Trans. Softw. Eng., SE-12(2):251–257, February 1986.
David L. Parnas and Jan Madey. Functional Documentation for Computer Systems. Science of Computer Programming, 25(1):41–61, October 1995.
A. van Lamsweerde and E. Letier. Integrating obstacles in goal-driven requirements engineering. In Proc. 20th Intern. Conf on Software Eng. (ICSE ‘98), Kyoto, Japan, April 1998.
V. Winter, R. Berg, and J. Ringland. Bay Area Rapid Transit District Advanced Automated Train Control System: Case Study Description. Sandia National Laboratories, 1999.
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
Heitmeyer, C. (2001). Using SCR to Specify Requirements of the Bart Advanced Automated Train Control 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_7
Download citation
DOI: https://doi.org/10.1007/978-1-4615-1391-9_7
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4613-5530-4
Online ISBN: 978-1-4615-1391-9
eBook Packages: Springer Book Archive