Process Algebra to Model Probabilistic Behavior of Smart IoT
Prof. Dr. Moonkun Lee, Chonbuk National University, Korea
Abstract
In general, process algebra can be the most suitable formal method to specify IoT systems due to the equivalent notion of processes as things. However there are some limitations to predict smart IoT systems with the properties of distribution, mobility and real-time. For example, Timed pi-Calculus has capability of specifying time property, but is lack of direct specifying both execution time of action and mobility of process at the same time. And d-Calculus has capability of specifying mobility of process itself, but is lack of specifying various time properties of both action and process, such as, ready time, timeout, execution time, deadline, as well as priority and repetition. In order to overcome the limitations, this lecture presents a process algebra, called, dTp-Calculus, extended from d-Calculus, by providing with capability of specifying probabilistic transitions with the set of time properties, as well as priority and repetition. Further the method is implemented as a tool, called SAVE, on the ADOxx meta-modeling platform. It can be considered one of the most practical and innovative approaches to model probabilistic behavior of smart IoT systems.
Supporting Business Process Improvement through a Modeling Tool
Prof. Dr. Florian Johannsen, Hochschule Schmalkalden, Germany
Abstract
Business Process Improvement (BPI) ranks among the topics of highest priority in modern organizations. However, considering the rapidly changing customer requirements in times of high market transparency and the increasing collaboration between organizations, the conduction of BPI projects has become very challenging. Implicit process knowledge from diverse process participants needs to be elicited and transformed into improvement opportunities. In this context, the results achieved need to be properly documented, communicated and processed throughout a company. The purpose of the lecture is to present a conceptual solution (called “BPI roadmap”), which is a means for systematically performing BPI initiatives based on a set of easy-to-use and proven BPI techniques. In the in the tool “RUPERT” (Regensburg University Process Excellence and Reengineering Toolkit), the BPI techniques are realized in form of corresponding model types. The lecture gives insights into the development of the “BPI roadmap” and “RUPERT” and demonstrates the tool’s functionality by referring to a use case stemming from a cooperation project.
Capability Oriented Requirements Engineerings
Prof. Evangelia Kavakli, University of the Aegean, Greeces
Abstract
The NEMO 2019 lecture concerns an approach to the application of conceptual modelling known as the Capability Oriented Requirements Engineering (CORE) approach. The conceptual modelling framework applied in CORE employs a set of complimentary and intertwined modelling paradigms based on enterprise capabilities, goals, actors, and information objects. The lecture will define the foundational concepts of CORE as well as the way of working from capturing textual descriptions from stakeholders, progressing to formally defining models of early requirements, based on the CORE meta-model, and in a stepwise refinement define functional and non-functional requirements of desired systems. The theory will be supplemented by examples from a real application of CORE on a Cyber Physical Production System.
Capability Oriented Requirements Engineerings
Prof. Evangelia Kavakli, University of the Aegean, Greeces
Abstract
The NEMO 2019 lecture concerns an approach to the application of conceptual modelling known as the Capability Oriented Requirements Engineering (CORE) approach. The conceptual modelling framework applied in CORE employs a set of complimentary and intertwined modelling paradigms based on enterprise capabilities, goals, actors, and information objects. The lecture will define the foundational concepts of CORE as well as the way of working from capturing textual descriptions from stakeholders, progressing to formally defining models of early requirements, based on the CORE meta-model, and in a stepwise refinement define functional and non-functional requirements of desired systems. The theory will be supplemented by examples from a real application of CORE on a Cyber Physical Production System.
Quality Assurance for BPMN Models
Prof. Dr. Andreas Polini, University of Camerino, Italy
Abstract
Business Process modelling has acquired increasing relevance in software development. Available notations, such as BPMN, permit to describe the flow of activities of complex organisations, when they are pursuing specific objectives. On the one hand, this shortens the communication gap between domain experts and IT specialists. On the other hand, this permits to clarify the characteristics of software systems introduced to provide automatic support for such activities. Nonetheless the lack of a formal semantics hinders the adoption of the standard by software engineers, as it leaves room for ambiguity and it limits the possibility to precisely check the satisfaction of relevant behavioural properties. In both cases with a negative impact on the quality of the resulting software. The lecture will introduce a verification framework for BPMN, called BProVe, that is based on a structured operational semantics definition, implemented using the executable formal framework MAUDE. The specification has been devised to clarify the semantics of the language, and to make the model verification possible and effective. With the intention to effectively support BPMN model verification, also on those scenario suffering from the state-space explosion problem, BProVe integrates both standard model checking techniques, through the MAUDE's LTL model checker, and statistical model checking techniques, through the statistical analyzer MultiVeSta. To support the adoption of the framework a complete toolchain that allows for rigorous modelling and verification of business processes has been developed. In the lecture practical examples will be used, and successively a set of exercises will be proposed to students that will have the opportunity to use the proposed tool chain.