Monitoring the correctness of distributed cyber-physical systems is essential. We address the analysis of the log of a black-box cyber-physical system. Detecting possible safety violations can be hard when some samples are uncertain or missing. In this work, the log is made of values known with some uncertainty; in addition, we make use of an over-approximated yet expressive model, given by a non-linear extension of dynamical systems. Given an offline log, our approach is able to monitor the log against safety specifications with a limited number of false alarms. As a second contribution, we show that our approach can be used online to minimize the number of sample triggers, with the aim at energetic efficiency.
The tool MoULDyS is based on the following paper:
Offline and Online Monitoring of Scattered Uncertain Logs Using Uncertain Linear Dynamical Systems. Bineet Ghosh, Étienne André. In: Formal Techniques for Distributed Objects, Components, and Systems (FORTE). 2022.
MoULDyS: A tool to perform monitoring of autonomous systems.- Checkout the
MoULDySwebpage here. - Given a bounding model of the system,
MoULDyScan perform online and offline monitoring:- Offline Monitoring:
MoULDyScan analyze a given log to detect possible safety violations, that might have caused the failure.- What kind of logs can
MoULDyShandle?- A log comprises of recorded samples, which can have samples missing at various time steps, and also the recorded samples can have added noise to it due to sensor uncertainties.
- What kind of logs can
- Online Monitoring:
MoULDyShas a framework to infer safety of a system that triggers the logging system to sample only when needed. This targets at energy efficiency by sampling only when required.
- Offline Monitoring:
- Interested in knowing more?
- Please feel free to checkout the website.
A detailed installation guide is provided in /documentation/installation_guide.md.
MoULDyS can be used in the following two ways:
- Virtual Machine Image (Recommended). This is the simplest way to use
MoULDyS, which does not necessitate the installation of any dependencies or code downloading. Nevertheless, it is required to acquire and install the Gurobi license. Users can recreate the results easily using this method. This also requires VirtualBox installed on the user's machine. TheMoULDySvirtual machine (VM) image can be downloaded from here. - Install
MoULDySon Local Machine. This option requires installation of the tool from scratch.
This is the simplest way to use MoULDyS, which does not necessitate the installation of any dependencies or code downloading. Nevertheless, it is required to acquire and install the Gurobi license. Users can recreate the results easily using this method. This also requires VirtualBox installed on the user's machine. The MoULDyS virtual machine (VM) can be downloaded from here.
Python 3.9.xNumPySciPympmath- Gurobi Python Interface:
-
Download the repository to your desired location
/my/location/: -
Once the repository is downloaded, please open
~/.bashrc, and add the lineexport MNTR_ROOT_DIR=/my/location/MoULDyS/, mentioned in the following steps:-
vi ~/.baschrc -
Once
.bashrcis opened, please add the location, where the tool was downloaded, to a path variableMNTR_ROOT_DIR(This step is crucial to run the tool):-
export MNTR_ROOT_DIR=/my/location/MoULDyS/
-
-
Once MoULDyS is installed following either of the two ways, the steps provided in the /docuementation/user_guide.md should run without any error.
Following are some of the crucial functionalities offered by this prototype tool:
- Given uncertain logs, perform offline monitoring.
- Online monitoring.
We offer to case studies:
To recreate the results given in the paper, please see /documentation/recreate_results.md. Here, we illustrate the Anesthesia case study, as the other one can be run in similar fashion.
-
cd src/recreate_results_from_paper/ -
python Anesthesia.py -compare
>> STATUS: Computing reachable sets as per monitors . . .
>> SUBSTATUS: Log Step: 0 / 93 Time Diff: 4
Set parameter Username
Academic license - for non-commercial use only - expires 2023-06-23
>> SUBSTATUS: Log Step: 1 / 93 Time Diff: 4
>> SUBSTATUS: Log Step: 2 / 93 Time Diff: 9
>> SUBSTATUS: Log Step: 3 / 93 Time Diff: 3
>> SUBSTATUS: Log Step: 4 / 93 Time Diff: 60
>> SUBSTATUS: Computing refinement at at time step 56
>> Safety: Unsafe at log step 4
>> Time Taken: 1.8150854110717773
>> STATUS: Performing online monitoring using reachable sets . . .
>> SUBSTATUS: Triggering a log at time 49 Time Taken (Diff): 2.8897838592529297
>> SUBSTATUS: Triggering a log at time 84 Time Taken (Diff): 1.5441653728485107
>> SUBSTATUS: Triggering a log at time 118 Time Taken (Diff): 1.4773943424224854
>> SUBSTATUS: Triggering a log at time 151 Time Taken (Diff): 1.4035592079162598
>> SUBSTATUS: Triggering a log at time 184 Time Taken (Diff): 1.3938045501708984
>> SUBSTATUS: Triggering a log at time 216 Time Taken (Diff): 1.3295047283172607
>> SUBSTATUS: Triggering a log at time 247 Time Taken (Diff): 1.23390531539917
>> SUBSTATUS: Triggering a log at time 278 Time Taken (Diff): 1.2304279804229736
>> SUBSTATUS: Triggering a log at time 308 Time Taken (Diff): 1.1959354877471924
>> SUBSTATUS: Triggering a log at time 338 Time Taken (Diff): 1.1893253326416016
.
.
.
>> SUBSTATUS: Triggering a log at time 1915 Time Taken (Diff): 0.504248857498169
>> SUBSTATUS: Triggering a log at time 1934 Time Taken (Diff): 0.4994475841522217
>> SUBSTATUS: Triggering a log at time 1953 Time Taken (Diff): 0.5091230869293213
>> SUBSTATUS: Triggering a log at time 1972 Time Taken (Diff): 0.5124149322509766
>> SUBSTATUS: Triggering a log at time 1991 Time Taken (Diff): 0.5127806663513184
>> Safety: Safe
>> Number of Logs: 84
>> Time Taken: 66.15031671524048
>> STATUS: Performed online monitoring using reachable sets!One should see the following plot:
Note: Visualization takes quite some time.
The results provided in the paper can be found in /my/location/Monitoring/output/FORTE22.


