Verification of a Controller for Bart: An Approach Based on Horn Logic and Denotational Semantics

  • Lawrence King
  • Gopal Gupta
  • Enrico Pontelli
Part of the The Kluwer International Series in Engineering and Computer Science book series (SECS, volume 577)


We present a semantics-based framework for verifying real-time con- trollers implemented in Ada. Our semantics-based framework uses techniques based on denotational semantics, logic programming, and partial evaluation. We illustrate our framework by verifying the correctness of the real-time controller for the Bay Area Rapid Transit System (BART). The main property we wish to verify is that if two consecutive trains start out with some minimum separation distance between them (that is deemed to be safe), then a safe distance is always maintained. This safe distance is dependent on a number of different variables, such as speed, acceleration, and track gradient. Our approach allows automatic derivation of a verification system from the Ada-implementation of the controller.


Logic Program Logic Programming Partial Evaluation Parse Tree Denotational Semantic 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. C. Consel. A tour of Schism: A partial evaluation system for higher-order applicative languages. Symp. on Partial Eval. and Semantics-Based Program Manipulation, 1993.Google Scholar
  2. P. Cousot, R. Cousot, “Abstract Interpretation: A Unified Model for Static Analysis of Programs for Construction or Approximation of Fix-points,” In Conference Record of the 4th ACM POPL, pp. 238–252, 1977.Google Scholar
  3. L.K. Dillon. Using symbolic execution for verification of Ada tasking programs. ACM TOPLAS. 12(4), 1990.Google Scholar
  4. G. W. Ernst, R. J. Hookway, J. A. Menegay, W. F. Ogden. Modular Verification of Ada Generics. In Computer Languages, 16(3/4): 259–280, 1991.Google Scholar
  5. J-P Finance (ed). Foundational Aspects of Software Engineering. Springer Verlag. 1999.Google Scholar
  6. D. Guaspari et al. Formal Verification of Ada Programs. TSE 16(9): 1058–1075, 1990.Google Scholar
  7. C. Gunter. Programming Language Semantics. MIT Press. 1992.Google Scholar
  8. G. Gupta “Horn Logic Denotations and Their Applications,” The Logic Programming Paradigm: A 25 year perspective. Springer Verlag. 1999.Google Scholar
  9. G. Gupta, E. Pontelli, et al. Automatic Derivation of a Provably Correct Parallelizing Compiler, Int. Conf, on Parallel Processing, IEEE Press, 1998.Google Scholar
  10. G. Gupta, E. Pontelli. A Constraint-based Denotational Approach to Specification and Verification of Real-time Systems. In Real-time Systems Symposium, IEEE, 1997.Google Scholar
  11. G. Gupta, E. Pontelli. A Horn Logic Denotational Framework for Specification, Implementation, and Verification of Domain Specific Languages. Tech. Report, NMSU, 1999.Google Scholar
  12. J. Jaffar, M.J. Maher. Constraint Logic Programming. In Journal of Logic Programming, Vol. 19/20, 1994.Google Scholar
  13. N. Jones. Introduction to Partial Evaluation. In ACM Computing Surveys. 28(3):480–503.Google Scholar
  14. N. G. Leveson et al. Safety Verification of Ada Programs Using Software Fault Trees. IEEE Software 8(4), 1991.Google Scholar
  15. J.W. Lloyd. Foundations of Logic Programming. Springer Verlag. 2nd ed. 1987.MATHCrossRefGoogle Scholar
  16. David C. Luckham, et al. Two-Dimensional Pinpointing: Debugging with Formal Specifications. IEEE Software 8(1): 74–84 (1991)MathSciNetCrossRefGoogle Scholar
  17. K. Marriott and P. Stuckey Constraint Programming MIT Press, 1997.Google Scholar
  18. M. Müller-Olm et al. Model checking: a tutorial introduction. Proc. Static Analysis Symp. Springer, 1999.Google Scholar
  19. W. Polak. Program Verification Based on Denotational Semantics. ACM POPL 1981. pp. 149–158Google Scholar
  20. D. Sahlin. An Automatic Partial Evaluator for Full Prolog. Ph.D. Thesis. 1991. Royal Institute of Technology.Google Scholar
  21. D. Schmidt. Denotational Semantics: a Methodology for Language Development. W.C. Brown Pub., 1986.Google Scholar
  22. D. Schmidt. Programming language semantics. In Handbook of Computer Science, CRC Press, 1996.Google Scholar
  23. L. Sterling, S. Shapiro. The Art of Prolog. MIT Press, 1994.MATHGoogle Scholar
  24. J. Stoy. Denotational Semantics: The Scott-Strachey Approach to Programming Languages. MIT Press. 1977.Google Scholar
  25. V. Winter et al. Bay Area Rapid Transit District Advance automated Train Control System: Case Study Description. Technical Report, Sandia National Labs, 1999.Google Scholar

Copyright information

© Springer Science+Business Media New York 2001

Authors and Affiliations

  • Lawrence King
    • 1
  • Gopal Gupta
    • 1
  • Enrico Pontelli
    • 1
  1. 1.Lab for Logic and Databases, Department of Computer ScienceNew Mexico State UniversityUSA

Personalised recommendations