Formal specification of real-time dependable systems

The complex and critical nature of real-time, dependable systems (henceforth referred to as RTD systems) necessitates the use of analyzable specifications and specification analysis techniques supporting the assessment of behavioral, safety-critical, security, and fault-tolerant qualities of systems. The need to rigorously state and analyze RTD system specifications suggests the use of formal specification techniques (FSTs), that is techniques that provide a precise specification language and specification analysis mechanisms based on formal reasoning systems. Unfortunately, most current FSTs focus on specifying functionality, and neglect non-functional qualities such as fault tolerance and security. While there is much research on extending FSTs so that they can be applied to non-functional properties, little work has gone into developing integrated sets of FSTs that can be applied throughout the development of RTD systems. We discuss how FSTs can be utilized in a multilevel description of RTD systems. FST´s make possible rigorous analysis at each level and rigorous consistency check across the levels