Software Tools If you find some tools missing or you want to add your tool to the list, please forward the link of the tool together with a brief description to [email protected]. Software Description Keywords BZR BZR is a reactive language, belonging to the synchronous languages family, whose main feature is to include discrete controller synthesis within its compilation. It is equipped with behavioral contract mechanisms, where assumptions can be described, as well as an "enforce" property part: the semantics of this latter is that the property should be enforced by controlling the behaviour of the node equipped with the contract. This property will be enforced by an automatically built controller, which will act on free controllable variables given by the programmer. BZR is developed in the Ctrl-A team. FSA, Supervisory Control, Controller Synthesis CIF (part of Eclipse ESCET) CIF is a declarative modeling language for the specification of discrete event, timed, and hybrid systems as a collection of synchronizing automata. The CIF tooling supports the entire development process of controllers, including among others specification, supervisory controller synthesis, simulation-based validation and visualization, verification, real-time testing, and code generation. Combined they enable a synthesis-based engineering approach to efficiently and cost-effectively design and implement high-quality controllers. Extended-FSA, Supervisory, Supervisor Synthesis, Hybrid Automata, Simulation, Model-based Systems Engineering DECADA DECADA is a tool for analyzing the control and diagnosis issues in discrete-event systems. FSA, Fault Diagnosis, Supervisory Control DECK Discrete Event Control Kit (DECK) is a toolbox (set of M-file functions) written in the programming language of MATLAB for the analysis and design of supervisory control systems based on discrete-event models. Supervisory Control, FSA DESlab DESlab is a scientific computing program written in python for the development of algorithms for analysis and synthesis of discrete event systems (DES) modeled as automata. FSA, Supervisory Control DESpot DESpot is a discrete-event system (DES) software research tool. It supports both flat projects (collection of plant and supervisor DES), and Hierarchical Interface-Based Supervisory Control (HISC) projects. FSA, Supervisory control, Hierarchical DESUMA The Discrete Event System, University of Michigan and Mount Allison University, or DESUMA, is a software and educational tool used to build, analyze and control models of Discrete Event Systems (DES) as finite-state automata (FSA). FSA, Fault Diagnosis, Supervisory Control DPO-SYNT DPO-SYNT is a C++ based software toolbox for property enforcement for partially-observed Discrete Event Systems. It implements a recently developed uniform framework for synthesizing maximally-permissive supervisors and optimal sensor activation policies. FSA, Supervisory Control, Sensor Activation edisyn EdiSyn is a Python-based toolkit for synthesizing obfuscators that enforces privacy while preserving utility with formal guarantees. Obfuscator Synthesis, Privacy Enforcement ePNK The ePNK is a platform for developing Petri net tools based on the PNML transfer format. Its main idea is to support the definition of Petri net types, which can be easily plugged into it, and to provide a simple generic GMF editor, which can be used for graphically editing nets of any plugged in type. P/T Nets, Model Checking GPenSIM GPenSIM is a flexible, user-friendly, and powerful tool that runs on MATLAB platform. Due to its flexibility, it is easy to create newer Petri net extensions with GPenSIM. Petri Nets, Simulation IDES IDES is a software tool developed at Queen’s University for modeling discrete-event systems and solving discrete-event control systems problems. It allows you to mimic pen-and-paper drawing of state-transition diagrams, export your drawings to a variety of formats such as EPS, JPEG, LaTeX and Grail+, and perform DES operations. FSA, Supervisory Control, Directed Graphs libFAUDES The discrete event systems library libFAUDES implements data structures and algorithms for finite automata and regular languages. Supervisory control, FSA MDESops MDESops is an open-source tool written in Python for analysis and control of discrete event systems modeled as finite-state automata. It includes a growing set of operations on automata, including: (i) manipulation of models (e.g., parallel composition, observer); (ii) diagnosis and opacity verification; (iii) common supervisory control functions (e.g., computation of supremal controllable and normal sublanguages); and (iv) more advanced functions on synthesis of attackers and of resilient supervisors in the presence of sensor deception attacks. The repository is a Git server maintained by the EECS Department at the University of Michigan, USA. FSA, supervisory control, diagnosis, opacity, cyber-security MinMaxGD MinMaxGD-a library to handle perioidic series in dioid of formal series. There are a C++ version and an interface with Scicoslab. Max-Plus, Periodic Series in dioid PRISM PRISM is a probabilistic model checker, a tool for formal modelling and analysis of systems that exhibit random or probabilistic behaviour. Model Checking, Probabilistic Systems ReaX ReaX is a tool for controller synthesis of symbolic logico-numerical systems. It makes use of abstract interpretation techniques to handle infinite-state systems (that involve state variables defined on infinite domains such as Integers or Rationals); it also efficiently handles finite-state ones. Controller Synthesis, Infinite-State Systems Roméo Roméo is a software studio for Time Petri Net analysis, developed in the Real-Time Systems Team at IRCCyN . It performs analysis on T-Time Petri nets and on one of their extension to scheduling. Time Petri Nets, Model Checking SCOTS SCOTS is a tool for the automatic controller synthesis of nonlinear control systems based on symbolic models. The tool accepts a differential equation as the description of a nonlinear control system. It uses a Lipschitz type estimate on the right-hand-side of the differential equation together with a number of discretization parameters to compute a symbolic model. The tool supports the computation of minimal and maximal fixed points and thus natively provides algorithms to synthesize controllers with respect to invariance and reachability specifications. Controller Synthesis, Nonlinear Systems, Symbolic Methods SENSE SENSE is a tool for the automatic controller synthesis of complex plants in the networked control systems (NCS) based on symbolic models. The tool accepts an existing symbolic model of a nonlinear plant in the NCS and the network characteristics. It computes a symbolic model of the overall networked control system. The tool supports the computation of minimal and maximal fixed points and thus natively provides algorithms to synthesize controllers with respect to invariance and reachability specifications. Controller Synthesis, Networked Systems, Symbolic Methods Supremica Supremica is a tool for automatic verification and synthesis of controllers for discrete event systems. Extended-FSA, Synthesis, Abstraction, Verification SuSyNA This tool allows a user to perform standard supervisor synthesis and time-weighted synthesis plus functions for observer-check and DOT file generation. Supervisor Synthesis, FSA, Time-Weidghted Systems TAKOS TAKOS stands for Java Toolbox for Analyzing the K-Opacity of Systems dedicated to the analysis, the runtime verification and enforcement of opacity on systems. Opacity, Runtime Verification & Synthesis TCT TCT is a tool for synthesis of controllers for discrete event systems. FSA, Supervisory Control Teloco Teloco (TEst of LOgic COntrollers) is an academic tool that permits to generate a conformance test sequence from an industrial specification in IEC 60848 language (GRAFCET). Technically, the specification model is first automatically translated, without semantics loss, into an equivalent Mealy machine. A minimum-length test sequence is then automatically generated from this machine. This sequence can afterwards be used for black-box conformance test of Programmable Logic Controllers (PLC) with cyclic I/O scanning. This tool has been developed in the frame of a project funded by the French Research Agency. PLC, Conformance Testing TINA TINA (TIme petri Net Analyzer) is a toolbox for the editing and analysis of Petri Nets, with possibly inhibitor and read arcs, Time Petri Nets, with possibly priorities and stopwatches, and an extension of Time Petri Nets with data handling called Time Transition Systems Time Petri Nets, Analysis TuLiP The Temporal Logic Planning (TuLiP) toolbox is a Python package for automatic synthesis of correct-by-construction embedded control software. Temporal Logic, Synthesis UPPAAL Uppaal is an integrated tool environment for modeling, validation and verification of real-time systems modeled as networks of timed automata, extended with data types (bounded integers, arrays, etc.). Timed Automata, Verification VEiP VEiP is a Java based toolbox for verification and enforcement of opacity properties formulated in Discrete Event Systems. Opacity, Verification, Enforcement VeriSiMPL This toolbox is used to generate finite abstractions of autonomous Max-Plus-Linear (MPL) models over R^n. Abstractions are characterized as finite-state Labeled Transition Systems (LTS). MPL Systems, Abstraction WOLFGANG Wolfgang is a lightweight tool that allows users to easily create and edit Petri nets and check them against general and workflow specific net properties. P/T-Nets, Colored Petri Nets A list of related tools provided by the IEEE CSS TC on Hybrid Systems can be found here. A more comprehensive list of Petri Nets Tools can be found here. A more comprehensive list of Model Checkers can be found here. Useful Links IFAC Technical Committee 1.3 on Discrete Event and Hybrid Systems Journal of Discrete Event Dynamic Systems Theory and Applications Workshop Series on Discrete Event Systems
