# Semantic Modeling Approach Supporting Process Modeling and Analysis in Aircraft Development
## 3 Semantic Modeling Approach for Process Modeling and Analysis
### Process Analysis Based on KARMA Formalism
#### 3.3.2 Dynamic Analysis for Process Model  
Hybrid automaton refers to a finite state machine with continuously evolving variables and discrete jump transitions to describe the dynamic behavior of a system. [PERSON] et al. attempted to describe the hybrid automation using KARMA language in the method level to support dynamic analysis [PERSON] et al. (2018). On the basis of their method, we use it in the practice of process modeling. In our research, the continuous system state and discrete event system features in the process model for verification are defined. The continuous system state describes the variables of the parameter state in the system evolution with time and events, for example, vehicle speed and mileage are physical quantities that change continuously with time [PERSON] et al. (2018). The discrete event system refers to a dynamic system that is driven by events and changes the state of the system by leaps and bounds [PERSON] et al. (2018). The behavior of discrete systems is generally described by formal models such as logic and algebra. The hybrid automaton is a generalized finite-state automaton that is furnished with continuous variables. The syntax of hybrid automata is expressed as [PERSON] et al. (2018)  
\[H=<Loc,Edg,\Sigma,X,Init,Inv,Flow,Jump>\]  
* _Loc_ is a finite set \(\{l_{1},l_{2},...l_{n}\}\) of system discrete states;
* \(\Sigma\) is a finite set of event names;
* _Edge_\(\subseteq Loc\times\Sigma\times Loc\) is a finite set of labeled edges which represent discrete changes;
* \(X\) is a finite set \(\{x_{1},x_{2},..x_{m}\}\) of real-valued variables; \begin{table}
\begin{tabular}{l l l} \hline \hline
**Class** & **Description** & **Syntax** \\ \hline SMTAnalysis & Declare the module of analysis & SMTAnalysis \textless{Name}\textgreater{} \\  & for property verification. &... \\  & & end \textless{Name}\textgreater{} \\ \hline PropertyState & Capture the value of property & languageID. modelID. \\  & instance. & ObjectID. \\  & & Property[PropertyID] \\ \hline  & & Int a; \\  & & Int b = valueOf(); \\  & & Boolean x; \\ VariableDeclare & Declare the variables. & Boolean y = true; \\  & & Matrix m = IntegerMatrex; \\  & & Matrix n = [1,1;2,2]; \\  & &... \\ \hline SolveDeclare & Declare that the property verification & Solve \textless{Name}\textgreater{} \\  & type is to evaluate the &... \\  & satisfiablity of constraints. & end \textless{Name}\textgreater{} \\ \hline OptimizeDeclare & Declare that the property verification & Optimize \textless{Name}\textgreater{} \\  & type is to optimize the variable &... \\  & value of property instances. & end \textless{Name}\textgreater{} \\ \hline solveStatement & Indicate the statements of how to & \textless{Name}\textgreater{}add(a\&\&\textless{(\textgreater{}b,...))}\textgreater{} \\  & evaluate the constraints. & //construct a temporary \\  & & stack; \\  & & \textless{Name}\textgreater{}check; \\ \hline optimizeStatement & Indicate the statements of how to & \textless{Name}\textgreater{}p\textgreater{}; \\  & optimize the constraints. & \textless{Name}\textgreater{}Max(a+b); \\  & & \textless{Name}\textgreater{}solution; \\ \hline \hline \end{tabular}
\end{table} 
Table 3: Syntax of KARMA Language for static analysis. * \(Init,Inv,Flow\) are functions that assign three predicates to each location. \(Init\) and \(Inv\) define sets of initial states and invariants that set value constraints for each state, respectively. \(Flow\) is a set of predicates that defines the continuous evolution of the hybrid system in one state;
* \(Jump\) is a function assigning to each labeled edge a predicate that provides discrete events when a hybrid automaton moves from one state to another. In the KAMRA language, the mapping expression of the hybrid automaton \(H\) is realized, in which \(Loc\), \(Init\), \(X\) and \(Inv\) are mapped to the object metamodels, and \(Edg\), \(Flow\), \(Jump\), and \(\Sigma\) are mapped to the relationship metamodels.