Research History and Publications Sample Clauses

Research History and Publications. As mentioned before, the goal of this thesis is to find a formal verification framework for component based systems in general and for their coordination subsystems in particular. We have chosen model checking of temporal logic properties as the verification method. From a historical point of view, our research can be divided into four periods or steps: • In the first step, our focus was on working on constraint automata as the operational semantics of coordination systems and as the models of the interfaces of components. Thus, in this phase, our aim was to prepare a compositional and hierarchal environ- ment for model checking of linear time properties of constraint automata models in the presence of the state explosion problem. Our main ideas to do this were presented in [82, 77]. To tackle the state explosion problem, we investigated two different solution methods: – Compositional minimization of models using suitable equivalence relations. For this aim, in [79, 78] we introduced two failure-based equivalence relations CFFD and NDFD as new semantics for constraint automata and our proposal for us- ing them to reduce the size of models for model checking. We also proved that CFFD and NDFD are congruences with respect to join and hiding composition operators of constraint automata [75, 74]. Moreover, we showed that the temporal logics preservation and minimality properties of CFFD and NDFD hold for the case of constraint automata [76]. Based on these results, we introduced a method for compositional model checking of component based systems, reduction algo- rithms, and their implementations and application to case studies [76, 69]. – As another way to deal with the state explosion, we considered abstraction tech- niques. In this method, using some suitable mapping from a large state space into a smaller one that preserves desired sets of linear temporal properties, we try to do model checking over the smaller model. A suitable mapping can be obtained by reducing the number of state variables from the model whose state variables are more to another one with less variables. Suitable mappings preserve linear time fairness and liveness properties [69, 119, 118]. • In the second step, based on the shortcomings of constraint automata in modeling all aspects of the behavior of connectors and the complication of their timed data streams based semantics, we focused on presenting a new operational semantics for Reo and on their model checking. Our main motivation ...