Zone-based specificAtion and veriFication of rEal-time self-adapTive sYstems.
The ZAFETY framework is a Zone-based approach to specify and verify real-time self-adaptive systems. It relies on a zone-based modeling technique to support separation of concerns. The formalism is called zone-based Time Basic nets (an extension of Time Basic Petri nets). The zones identified during the modeling phase can be used as modules either in isolation, to verify intra-zone properties, or all together, to verify inter-zone properties over the entire system. In addition, the framework allows the verification of (timed) robustness properties to guarantee self-healing capabilities when higher levels of reliability and availability are required to the system, especially when dealing with time-critical systems.
The ZAFETY software tool architecture is presented in the figure below.
The ZAFETY editor is a customized version of PIPE2. It supplies a graphical user interface to create and edit arbitrary complex zone-based TB net models. A drawing toolbar allows the user to draw a model into the main canvas through simple drag and drop gestures.
The ZAFETY engine has been implemented on top of Graphgen. The TRG builder exploits the components of Graphgen in order to create the reachable symbolic states of a TB net model. Given a PNML file, it generates as output the TRG (along with regions) in binary format that can be used in turn by the formal verification module. The tool can also create an annotated text format, used by the GraphViz software tool to generate a graphical visualization of the TRG.
The formal verification component grants the possibility of verifying the conformance of the behavior against intended adaptation models by means of cross-zone transition properties. Moreover, it supports the verification of timed properties in order to check real-time constraints, and it supports the verification of robustness properties to verify time-constrained self-healing behaviors.
Use the following reference to cite this work:
The source code of the ZAFETY engine is available at https://bitbucket.org/zafety/zafety-engine. The repository contains the TRG builder and the formal verification components, and some zone-based TB net examples.
ZAFETY is free software: you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation, either version 3 of the License, or (at your option) any later version. ZAFETY is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details. You should have received a copy of the GNU General Public License along with ZAFETY. If not, see http://www.gnu.org/licenses/.
The ZAFETY repository (resources package) contains two main examples: the gas burner (GB) and the unmanned aerial vehicle (UAV). To view and edit these models you can use the ZAFETY editor (download the jar archive).
The Executable jar archive of the ZAFETY engine is available for download.
To build the TRG of the GB example you can type:
You can find the output in the same directory of the model: "adaptive-gb.graph" (binary format) and "adaptive-gb.dot" (DOT file).
java -jar zafety-engine.jar -m adaptive-gb.xml
To run the formal verification module of the ZAFETY engine you can type:
You can verify, for instance, the following properties: Structural properties:
java -jar zafety-engine.jar -c -m adaptive-gb.xml -g adaptive-gb.graph
Cross-zone transition properties:
Safety adaptation meta-properties:
overlap(#NORMAL, IgnFail, #UNDESIRED)
Robustness adaptation meta-properties:
!(#NORMAL ?> #INVALID)
#NORMAL ?> #UNDESIRED
#UNDESIRED −> #RECOVERY
Timed adaptation meta-properties:
#RECOVERY −> #NORMAL
#NORMAL ?> #UNDESIRED, 1.25
Invariants, safety and liveness (timed) intra-zone properties:
#UNDESIRED −> #RECOVERY, 0.6
A(Gas!=1 || NoGas==0)
!E(Idle==1 && Gas==1)
Invariants, safety and liveness (timed) inter zone properties:
IgnActReq==1 && ValActOpen==1 −> Gas==1 && Ignition==1, 0.6
A(Gas!=1 || (NoGas==0 && NoGas2==0))
!E(Idle==1 && (Gas==1 || Gas2==1 || Gas3==1))
FailureDetection==1 −> CloseValvActReq==1 && AirOnActReq==1, 0.4