Paper Info
Title
A Method for Verifying Real-Time Properties of Ada Programs
Abstract
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.
Year
DOI
Venue
2001
10.1109/ICECCS.2001.930162
ICECCS
Keywords
Field
DocType
uppaal model checker,concurrent program,verifying real-time properties,ada programs,tla specification,typical client user task,concurrent ada program,ada implementation,icpp scheduling,abstract variable,complex data structure,various task,timed automaton,automata,computer science,computer languages,complex data,ada,automata theory,real time,data structures,control structure,concurrent computing,worst case execution time,real time systems,scheduling,object oriented languages,real time system,kernel
Data structure,Automata theory,Programming language,Model checking,Object-oriented programming,Computer science,Automaton,Real-time computing,Real-time operating system,Timed automaton,Concurrent computing
Conference
Citations 
PageRank 
References 
1
0.40
8
Authors
2
Name
Order
Citations
PageRank
thorsten gerdsmeier160.86
Rachel Cardell-Oliver227133.25