A simplification of a real‐time verification problem. (10th October 2016)

• Record Type: Journal Article
• Authors: Roy, Suman; Misra, Janardan; Saha, Indranil
• Is Part Of: Software testing, verification & reliability. Volume 26:Number 8(2016)
• Page Start: 548
• Page End: 571
• Publication Date: 2016-10-10
• Subjects: real‐time systems -- model checking -- timeout and calendar model -- digitization -- finite state verification -- temporal logics; Computer software -- Testing -- Periodicals; Computer software -- Verification -- Periodicals; Computer software -- Reliability -- Periodicals; 005.14
• DOI: 10.1002/stvr.1622
• Languages: English
• ISSNs: 0960-0833

Abstract

Summary: We revisit the problem of real‐time verification with dense‐time dynamics using timeout and calendar‐based models and simplify this to a finite state verification problem. We introduce a specification formalism for these models and capture their behaviour in terms of semantics of timed transition systems. We discuss a technique, which reduces the problem of verification of qualitative temporal properties on infinite state space of a large fragment of these timeout and calender‐based transition systems into that on clock‐less finite state models through a two‐step process comprising of digitization and finitary reduction. This technique enables us to verifysafety invariants for real‐time systems using finite state model checking avoiding the complexity of infinite state (bounded) model checking and scale up models without applying techniques from induction‐based proof methodology. In the same manner, we verify timeliness properties. Moreover, we can verifyliveness for real‐time systems, which are not possible by using induction with infinite state model checkers. Copyright © 2016 John Wiley & Sons, Ltd. Abstract : In this work we propose a technique for reducing the problem of infinite state verification of qualitative temporal properties on timeout and calendar based transition systems to the problem of finite state verification of the same properties on those models. The technique is comprised of two steps, digitization of infinite state system with continuous time dynamics to the same with discrete time dynamics, and a finitary reduction of the latter to a finite state clock‐less system. This technique enables us to verify safety, liveness and timeliness properties of the system with finite state model checkers.