Modeling and Verification for Timing Satisfaction of Fault-Tolerant Systems With Finiteness
Source: TECHNICAL UNIVERSITY OF MUNICH
The complexity of distributed real-time systems is growing rapidly; model-based development tools are used to accelerate the development process and increase the quality of the produced code. In addition, it is possible to integrate formal verification as analysis technique into these tools. Currently, the standard verification process is achieved by first translating system models into verification models, followed by verifying relevant properties by verification engines using special algorithms. In the verification community, researchers focus on tighter theoretical complexity bounds or computationally faster algorithms to reduce the required time for verification. Nevertheless, if it comes to verification of complex systems, an efficient model reflecting the properties of the system under consideration becomes essential.