A Timed Analysis Technique for Single Processor Real-Time Systems

This paper presents a time modeling technique for timing verification and analysis of single processor real-time systems with non-preemptive schedulers. Time is considered to be orthogonal to the underlying untimed CSP, and is introduced using as few as possible modifications. Although more restrictive and less expressive than previously proposed time modeling techniques, our methodology produces smaller finite models which result in faster verification for the class of systems it is designed for. An efficient implementation of the proposed algorithms based on the ARC tool and early experimental results are also presented. 1 Introduction Many existing real-time applications are also of a safety-critical nature. With the ever increasing complexity of such systems meeting all of their stringent requirements is not a trivial task at all. Formal methods can alleviate some of the difficulties associated with the specification, design and verification of such systems by putting them on a s..