The BPMN standard notation allows business process designers to model both intra-organizational processes and inter-organizational collaborations. A great effort has been devoted in proposing formal ...semantics for BPMN, and, fewer, in providing dedicated verification tools. Still, some advanced features of BPMN, namely communication or time-related constructs, are often set aside. This becomes an issue as BPMN gains interest outside of its original scope, e.g., for the IoT where communication and time play an important role. In this paper, we propose a formal semantics for a subset of BPMN. This semantics takes into account not only the usual gateways, but also sub-processes, inter-process communication, and time-related constructs. In contrast to transformational approaches, which give a semantics to BPMN by mapping it to some formal model (e.g., transition systems or Petri nets), our approach is based on a direct formalization in first-order logic that is then realized in a straightforward way into the TLA+ formal language. We build on the TLA+ model-checker, TLC, to provide process designers with a verification framework, fbpmn, that one may use to check BPMN and workflow specific properties. Our tools and our model database are open source and freely available online.
•A direct formal semantics for a subset of BPMN, including sub-processes, communication and time constructs.•Automated verification of intra-organization workflows and inter-organization collaborations.•Seven models for communication, two models for time.•Communication models and properties of interest are easily extensible.•Open source and freely available tools and model repository.
The use of formal methods in the development of software aims to guarantee the software reliability. However, these formal methods stay limited at the specification and high level stages in the ...development cycle. The critical last step which translates the formal specification into source code stays manual and error prone. The formalisation and the automation of the translation from high level specification towards source code is an ambitious idea. In this paper, a general framework for an automated model transformation system is presented. The code-generator tool is intended for WSNs applications. It demonstrates that a correct source code of WSNs application can be synthesis from formal specification, automatically. The proposed framework accepts a formal specification of the WSNs system written in Timed Automata and generates the corresponding source code written in NesC language. The code-generator is based on a set of transformation rules. In this paper, we present the transformation approach, the implemented tool and a case study demonstrating its usability.
PDF
