Abstract
Keywords:
real-time systems, validation, partial knowledge, polyhedra.
Abstract:
Real-time embedded systems are used in highly important or even vital tasks (avionic and medical systems, etc.), thus having strict temporal constraints that need to be validated. Existing solutions use temporal logic, automata or scheduling techniques. However, scheduling techniques are often pessimistic and require an almost complete knowledge of the system, and formal methods can be ill-fitted to manipulate some of the concepts involved in real-time systems. In this article, we propose a method that has the advantages of formal methods and some simplicity in manipulating real-time systems notions. This method is able to model and validate all the classical features of real-time systems, without any pessimism, while guaranteeing the end of the validation process. Moreover, its formalism enables to validate systems of which we have only a partial knowledge, and thus to validate or invalidate a system still under design. This latest point is very important, since it greatly decreases the cost of design backtracks.