Thumbnail
Access Restriction
Open

Author Strehl, Karsten
Source CiteSeerX
Content type Text
File Format PDF
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Subject Keyword Traffic Control ♦ Interval Decision Diagram ♦ System Configuration ♦ Timed Automaton ♦ Efficient Manipulation ♦ Introduction Especially ♦ Formal Verification ♦ Canonical Representation ♦ Timed Reachability Analysis ♦ Interval Diagram Technique ♦ Transition Behavior ♦ Real-time Symbolic Model ♦ Boolean Function ♦ Formal Method ♦ Real-time System ♦ Safety-critical Real-time Application ♦ Symbolic Real-time Verification ♦ Interval Diagram ♦ Similar Verification Technique ♦ Interval Mapping Diagram ♦ Medical Engineering ♦ Technical System
Description In this paper, we suggest interval diagram techniques for formal verification of real-time systems modeled by means of timed automata. Interval diagram techniques are based on interval decision diagrams (IDDs)---representing sets of system configurations of, e.g., timed automata---and interval mapping diagrams (IMDs)--- modeling their transition behavior. IDDs are canonical representations of Boolean functions and allow for their efficient manipulation. Our approach is used for performing both timed reachability analysis and real-time symbolic model checking. We present the methods necessary for our approach and compare its results to another, similar verification technique---achieving a speedup of 7 and more. 1 Introduction Especially for safety-critical real-time applications such as those in traffic control, medical engineering, or avionics, simulation often is not sufficient to guarantee the correctness of a technical system's model. In addition to simulation, formal methods are e...
Educational Role Student ♦ Teacher
Age Range above 22 year
Educational Use Research
Education Level UG and PG ♦ Career/Technical Study
Learning Resource Type Article
Publisher Date 1999-01-01
Publisher Institution Proc. RTCSA '99