Integrated Model-Checking for the Design of Safe and Efficient Distributed Software Commissioning

摘要

We present MADA, a deployment approach to facilitate the design of efficient and safe distributed software commissioning. MADA is built on top of the Madeus formal model that focuses on the efficient execution of installation procedures. Madeus puts forward more parallelism than other commissioning models, which implies a greater complexity and a greater propensity for errors. MADA provides a new specific language on top of Madeus that allows the developer to easily define the properties that should be ensured during the commissioning process. Then, MADA automatically translates the description to a time Petri net and a set of TCTL formulae. MADA is evaluated on the OpenStack commissioning.