Practical Verification of Real-time Systems
Alexandre David, Uppsala University
Available as pdf or ps.gz file
or contact Alexandre at firstname.lastname@example.org
Opponent: Parosh Abdulla
TIME: 10.15-12, Friday, Oct 12, 2001
PLACE: Room 2347, Information Technology, DoCS, Uppsala University
Formal methods are becoming mature enough to be used on non trivial
examples. They are particularly well fitted for real-time systems
whose correctness is defined in terms of correct responses at correct
times. Most common real-time systems are of reasonable size and can
therefore be handled by an automatic verification tool such as UPPAAL.
Unfortunately the application of such techniques is not widely spread.
This thesis presents advances in making formal techniques
more accessable technology for system development and analysis.
As the first contribution, we report on an industrial case study to
show that model checkers can be used for debugging and error
localization. We shall present a number of abstraction techniques
applied in the case study to avoid the state explosion problem.
As the second contribution, we have developed a hierarchical
extension of timed automata to enable more structured, compact, and
more complex descriptions of systems by the users. Such a hierarchical
representation is better suited for abstraction and expected to
give better searching algorithms. Finally we present a hybrid
animation system serving as a plug-in module for model-checkers
to improve features for modelling and simulation.
ARTES project: Hierarchical Design and Analysis of Timed Systems
Reference: Alexandre David, Practical Verification of Real-time Systems. Licentiate Theses from the Department of Information
Technology, 2001-13 October 2001. ISSN 1404-5117.