Advertisement

Validation, verification and implementation of timed protocols using AORTA

  • S. Bradley
  • W. D. Henderson
  • D. Kendall
  • A. P. Robson
Chapter
Part of the IFIP Advances in Information and Communication Technology book series (IFIPAICT)

Abstract

AORTA is an implementable timed process algebra which has been proposed as a design language for hard real-time systems. In this paper we show how AORTA can be used to design and model timed protocols, illustrated by the alternating bit protocol. We also describe tools which have been developed for simulation, verification and automatic implementation of AORTA systems, and outline a relationship between the formal models which are verified and the code which is generated.

Keywords

AORTA real-time verification communication protocol 

References

  1. Alur, R., Courcoubetis, C. and Dill, D. (1990) Model-checking for real-time systems, IEEE Fifth Annual Symposium On Logic In Computer Science, Philadelphia, pp. 414–425.Google Scholar
  2. Alur, R., Courcoubetis, C. and Dill, D. (1993) Model-checking in dense real-time, Infor-mation and Computation 104, 2 — 34.Google Scholar
  3. Bradley, S., Henderson, W. D., Kendall, D. and Robson, A. P. (1994a) Application-Oriented Real-Time Algebra, Software Engineering Journal 9(5), 201–212.CrossRefGoogle Scholar
  4. Bradley, S., Henderson, W. D., Kendall, D. and Robson, A. P. (1994b) Designing and implementing correct real-time systems, in H. Langmaack, W.-P. de Roever and J. Vytopil (eds), Formal Techniques in Real-Time and Fault-Tolerant Systems FTRTFT ’84, Lubeck, Lecture Notes in Computer Science 863, Springer-Verlag, pp. 228–246.CrossRefGoogle Scholar
  5. Bradley, S., Henderson, W. D., Kendall, D. and Robson, A. P. (1995a) Modelling data in a real-time algebra, Technical Report NPC-TRS-95–1, Department of Computing, University of Northumbria, UK. Submitted for publication.Google Scholar
  6. Bradley, S., Henderson, W. D., Kendall, D., Robson, A. P. and Hawkes, S. (1995b) A formal design and implementation method for systems with predictable performance, Technical Report NPC-TRS-95–2, Department of Computing, University of Northumbria, UK. Submitted for publication.Google Scholar
  7. Bradley, S., Henderson, W., Kendall, D. and Robson, A. (1994c) A formally based hard real-time kernel, Microprocessors and Microsystems 18 (9), 513–521.CrossRefGoogle Scholar
  8. Burch, J., Clarke, E., McMillan, K., Dill, D. and Hwang, L. (1992) Symbolic model check-ing: 1020 states and beyond, Information and Computation 98 (2), 142–170.MathSciNetCrossRefzbMATHGoogle Scholar
  9. Clarke, E., Emerson, E. and Sistla, A. (1986) Automatic verification of finite-state concur-rent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems 8 (2), 244–263.CrossRefzbMATHGoogle Scholar
  10. Cleaveland, R., Parrow, J. and Steffen, B. (1993) The concurrency workbench: A semantics-based tool for the verification of concurrent systems, ACM Transactions on Programming Languages and Systems 15 (1), 36–72.CrossRefGoogle Scholar
  11. Daws, C., Olivero, A. and Yovine, S. (1994) Verifying et-lotos programs with kronos.Google Scholar
  12. Emerson, E. and Clarke, E. (1982) Using branching-time temporal logic to synthesize synchronization skeletons, Science of Computer Programming 2 (3), 241–266.CrossRefGoogle Scholar
  13. Henzinger, T., Nicollin, X., Sifakis, J. and Yovine, S. (1994) Symbolic model checking for real-time systems, Information and Computation 111(2), 193–244.MathSciNetGoogle Scholar
  14. Leduc, G. and Léonard, L. (1993) A timed lotos supporting dense time domain and including new timed operators, Formal Description Techniques V, 87–182.Google Scholar
  15. McMillan, K. (1993) Symbolic Model Checking: An approach to the State Explosion Prob-lem Kluwer.CrossRefGoogle Scholar
  16. Milner, R. (1989) Communication and Concurrency, Prentice Hall, New York.zbMATHGoogle Scholar
  17. Moller, F. and Tofts, C. (1989) A temporal calculus of communicating systems, Technical Report ECS-LFCS-89–104, Edinburgh University.Google Scholar
  18. Nicollin, X., Sifakis, J. and Yovine, S. (1992) Compiling real-time specifications into ex-tended automata, IEEE Transactions of Software Engineering 18(9), 794–804.CrossRefGoogle Scholar
  19. Olivero, A. and Yovine, S. (1993) Kronos: A tool for verifying real-time systems - Users’guide and reference manual - draft 0.0.Google Scholar
  20. Park, C. Y. (1993) Predicting program execution times by analyzing static and dynamic program paths, Real-Time Systems 5 (1), 31–62.CrossRefGoogle Scholar
  21. Park, C. Y. and Shaw, A. C. (1991) Experiments with a program timing tool based on source-level timing schema, IEEE Computer 24 (5), 48–57.CrossRefGoogle Scholar
  22. Schneider, S., Davies, J., Jackson, D. M., Reed, G. M., Reed, J. N. and Roscoe, A. W. (1991) Timed CSP: Theory and practice, in J. W. de Bakker, C. Huizing, W. P. de Roever and G. Rozenberg (eds), Real-Time: Theory in Practice (REX workshop), Mook, Lecture Notes in Computer Science 600, Springer-Verlag, pp. 640–675.Google Scholar
  23. Yovine, S. (1993) Méthodes et Outils pour la Vérification Symbolique de Systèmes Temporisés, PhD thesis, Institut National Polytechnique de Grenoble.Google Scholar

Copyright information

© IFIP International Federation for Information Processing 1996

Authors and Affiliations

  • S. Bradley
    • 1
  • W. D. Henderson
    • 1
  • D. Kendall
    • 1
  • A. P. Robson
    • 1
  1. 1.Department of Computing, University of Northumbria at NewcastleUniversity of Northumbria at NewcastleEllison Place, Newcastle upon TyneUK

Personalised recommendations