Process Algebraic and Structural Operational Semantics Sample Clauses

Process Algebraic and Structural Operational Semantics. In addition to the above mentioned models, there are some other attempts to present formal semantics for component connectors. In the work of ▇▇▇▇▇▇▇ et al. [32] the semantics of components are defined by the expressions of a process algebra. These expressions carry out both positive (presence) and negative (absence) information about data in ports. Complex connectors are built from basic ones using some composition operators such as join, parallel composition, and interleaving. This work needs more investigation to before it can be used for the purpose of deductive verification and is not suitable for model checking. The model needs more enhancements to express some important fairness constraints. In the joint works of ▇▇▇▇▇▇, ▇▇▇▇▇▇ et al., reported in [91, 92, 93, 94], and [95], they map some semantic models for Reo, namely, constraint automata, timed constraint automata, and coloring semantics to the process algebraic specification language of mCRL2 [61] and show the correctness of their mappings. Also, they have build a tool for these mappings that is now a part of the tool-set Extensible (Eclipse) Coordination Tools (ECT) [2]. In another work, ▇▇▇▇▇▇▇ et al. [116] express the formal semantics of Reo connectors by a set of structural operational semantic rules. In general, this semantics is not a context dependent semantics, it carries only positive information. However, to express some con- text dependencies, specially for the lossy synchronous channel, the authors used extra more rules to remove undesired behavior. To be able to express more fairness or context dependent behavior the set of rules needs to be expanded.