Specification and analysis of dynamic systems using temporal logic

Abstract

Many modern systems show dynamic characteristics in a sense that they change their configuration dynamically during run-time. In object-oriented systems, for example, the configuration of objects and their links change to reflect the state of such systems. Unfortunately, few analysis techniques address the dynamic nature explicitly. Most of them abstract away the dynamic nature of systems. Thus, there is a gap between analysis result and the reality. The goal of this dissertation is to propose a specification and validation technique for dynamic systems. In particular, we note that there exist few researches on the property specification of dynamic systems. We propose a new temporal logic, called HDTL, for specifying the required property. By employing the notion of freeze quantifier, HDTL allows us to specify the correctness requirements of dynamic systems precisely. We suggest two analysis methods for HDTL. The first is trace checking which automatically analyzes whether an execution trace generated from a system is consistent with a specification written in HDTL. We show the experiments using two different languages; SDL, an international standard modeling language for communication systems, and Java, an implementation language. The second analysis is model checking. The behavior model of a system is described in Maude, a formal method tool that supports modeling of con-current object-oriented systems. We show how to perform model checking using the HDTL checker, originally developed for trace checking. The fact that HDTL specification can be used both in the trace checking, and in the model checking shows that HDTL specification is reusable. A model with relatively lower complexity can be model-checked with an HDTL formula. After refinement, the same formula can be used to validate the refined model or the implementation, by trace checking.