Title :
A method for verifying real-time properties of Ada programs
Author :
Gerdsmeier, Thorsten ; Cardell-Oliver, Rachel
Author_Institution :
Dept. of Comput. Sci., Essex Univ., Colchester, UK
Abstract :
This paper describes a method for transforming concurrent Ada programs by way of abstractions into input for the UPPAAL model checker for the purpose of analyzing the real-time properties of programs. The method depends on being able to compute the best and worst case execution times of procedures called by the various tasks in a concurrent program. It employs abstractions of actions to simplify the control structure of a task, abstractions of complex data structures to more abstract variables and abstractions to simplify clocks. The method is illustrated on an Ada implementation of a kernel implementing ICPP scheduling. A TLA specification of a typical client user task is derived that can be interpreted as an UPPAAL timed automaton
Keywords :
Ada; automata theory; data structures; object-oriented languages; program verification; real-time systems; scheduling; ICPP scheduling; TLA specification; UPPAAL model checker; clocks; concurrent Ada programs; data structures; execution times; program verification; real-time system; timed automaton; Automata; Clocks; Computer languages; Computer science; Concurrent computing; Data structures; Delay; Kernel; Sparks; System recovery;
Conference_Titel :
Engineering of Complex Computer Systems, 2001. Proceedings. Seventh IEEE International Conference on
Conference_Location :
Skovde
Print_ISBN :
0-7695-1159-7
DOI :
10.1109/ICECCS.2001.930162
