Modeling and analysis of real-time Ada tasking programs
- 1 January 1994
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 132-141
- https://doi.org/10.1109/real.1994.342723
Abstract
Proposes a model for real-time Ada tasking programs that naturally represents such features as processor sharing, priority preemption, and process suspension. We describe a semi-decision procedure for proving properties of the model that uses linear programming to determine the feasibility of paths explored during a state-space search of the program. We demonstrate the feasibility of this procedure by applying a prototype analyzer to several examples.Keywords
This publication has 15 references indexed in Scilit:
- Analyzing timing requirementsPublished by Association for Computing Machinery (ACM) ,1993
- Compiling real-time specifications into extended automataIEEE Transactions on Software Engineering, 1992
- Communicating real-time state machinesIEEE Transactions on Software Engineering, 1992
- A layered approach to automating the verification of real-time systemsIEEE Transactions on Software Engineering, 1992
- Experiments with a program timing tool based on source-level timing schemaComputer, 1991
- Modeling and verification of time dependent systems using time Petri netsIEEE Transactions on Software Engineering, 1991
- A unified high-level Petri net formalism for time-critical systemsIEEE Transactions on Software Engineering, 1991
- Deciding properties of timed transition modelsIEEE Transactions on Parallel and Distributed Systems, 1990
- A timed model for communicating sequential processesTheoretical Computer Science, 1988
- Safety analysis of timing properties in real-time systemsIEEE Transactions on Software Engineering, 1986