טכניון מכון טכנולוגי לישראל
הטכניון מכון טכנולוגי לישראל - בית הספר ללימודי מוסמכים  
Ph.D Thesis
Ph.D StudentPerelman Valeriya
SubjectOperational Semantics for Object-Process Methodology
DepartmentDepartment of Industrial Engineering and Management
Supervisor Professor Dov Dori
Full Thesis textFull thesis text - English Version


Abstract

Model-based engineering approaches are increasingly adopted for various systems engineering tasks. Leading characteristics of modeling languages include clarity, expressiveness and comprehension. Exact semantics of the modeling language used in a model-based framework is critical for a successful system development process. As some of the characteristics contradict each other, designing a ”good” modeling language is a complex task. Still, an important precondition for acceptance of a modeling language is that its semantics must be precisely and formally defined.

Object Process Methodology (OPM) is a holistic, integrated model-based approach to systems development. The applicability of the OPM modeling language was studied through modeling of many complex systems from disparate domains, including business processing, real-time systems architecture, web applications development and mobile agents design. Experience with OPM has underlined the need to enrich the language with new constructs. An adverse side effect of the increased OPM expressiveness was that it also became more complex and in some cases ambiguous or undefined.

In this work, we define operational semantics for the core of the OPM language using a clocked transition system (CTS) formalism. The operational semantics consists of an execution framework and a set of transition rules. The principles and rules underlying this framework provide for determining the timing of transitions to be taken in a system modeled in OPM. The set of transition rules, adjusted to the OPM rules, describe all the possible changes in the system state based on the current state of the system and the set of its inputs.

Similar works defining formal operational semantics include Statecharts by David Harel, formalizing UML Statecharts with combined graph-grammar and model transition system (MTS) by Varro et al., and formalizing activity diagrams for workflow models by translating the subject model into a format appropriate for a model checker. 

Well-defined operational semantics enables extending OPM with a wide range of testing tools, including model-based simulation, execution and verification. As a solid proof of concept, we have developed an OPM-to-SMV (Symbolic Model Verification) translation tool for models in the domain of Molecular Biology (MB), based on the OPM-CTS framework principles and a subset of the transition rules. Using this tool, a holistic OPM model describing both research hypothesis and facts from state-of-the-art MB papers can be translated into an SMV verification tool. The generated SMV model can be verified against specifications, based on information found in MB papers and manually inserted into the SMV tool.