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.
Chapter PDF
Similar content being viewed by others
References
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.
Alur, R., Courcoubetis, C. and Dill, D. (1993) Model-checking in dense real-time, Infor-mation and Computation 104, 2 — 34.
Bradley, S., Henderson, W. D., Kendall, D. and Robson, A. P. (1994a) Application-Oriented Real-Time Algebra, Software Engineering Journal 9(5), 201–212.
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.
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.
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.
Bradley, S., Henderson, W., Kendall, D. and Robson, A. (1994c) A formally based hard real-time kernel, Microprocessors and Microsystems 18 (9), 513–521.
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.
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.
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.
Daws, C., Olivero, A. and Yovine, S. (1994) Verifying et-lotos programs with kronos.
Emerson, E. and Clarke, E. (1982) Using branching-time temporal logic to synthesize synchronization skeletons, Science of Computer Programming 2 (3), 241–266.
Henzinger, T., Nicollin, X., Sifakis, J. and Yovine, S. (1994) Symbolic model checking for real-time systems, Information and Computation 111(2), 193–244.
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.
McMillan, K. (1993) Symbolic Model Checking: An approach to the State Explosion Prob-lem Kluwer.
Milner, R. (1989) Communication and Concurrency, Prentice Hall, New York.
Moller, F. and Tofts, C. (1989) A temporal calculus of communicating systems, Technical Report ECS-LFCS-89–104, Edinburgh University.
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.
Olivero, A. and Yovine, S. (1993) Kronos: A tool for verifying real-time systems - Users’guide and reference manual - draft 0.0.
Park, C. Y. (1993) Predicting program execution times by analyzing static and dynamic program paths, Real-Time Systems 5 (1), 31–62.
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.
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.
Yovine, S. (1993) Méthodes et Outils pour la Vérification Symbolique de Systèmes Temporisés, PhD thesis, Institut National Polytechnique de Grenoble.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1996 IFIP International Federation for Information Processing
About this chapter
Cite this chapter
Bradley, S., Henderson, W.D., Kendall, D., Robson, A.P. (1996). Validation, verification and implementation of timed protocols using AORTA. In: Dembiński, P., Średniawa, M. (eds) Protocol Specification, Testing and Verification XV. PSTV 1995. IFIP Advances in Information and Communication Technology. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-34892-6_13
Download citation
DOI: https://doi.org/10.1007/978-0-387-34892-6_13
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-5041-2925-1
Online ISBN: 978-0-387-34892-6
eBook Packages: Springer Book Archive