main
Differences
This shows you the differences between two versions of the page.
Both sides previous revisionPrevious revisionNext revision | Previous revision | ||
main [2021/02/26 10:06] – [Manual, structure of the tool] merlin | main [2021/12/13 13:04] (current) – [Access to EPMC] andrea | ||
---|---|---|---|
Line 1: | Line 1: | ||
====== EPMC - (An Extendible Probabilistic Model Checker, previously known as IscasMC) ====== | ====== EPMC - (An Extendible Probabilistic Model Checker, previously known as IscasMC) ====== | ||
===== Introduction ===== | ===== Introduction ===== | ||
- | EPMC is a successor of the model checker IscasMC which only focuses on PLTL model checking over MDP. | + | EPMC is a model checker for probabilistic models. It |
+ | EPMC supports Markov chains and Markov decision Processes (MDP), and properties specified in PCTL, PLTL and their combination PCTL*. It implements the efficient algorithm in particularly tuned to handle linear time properties, [[http:// | ||
The main characteristics of EPMC are the high modularity of the tool, the possibility to extend EPMC with plugins to add new functionalities, | The main characteristics of EPMC are the high modularity of the tool, the possibility to extend EPMC with plugins to add new functionalities, | ||
Line 8: | Line 10: | ||
---- | ---- | ||
- | ===== Models supported by ePMC ===== | + | ===== Models supported by EPMC ===== |
* Discrete Time Markov Chains (DTMCs) | * Discrete Time Markov Chains (DTMCs) | ||
* Markov Decision Processes (MDPs) | * Markov Decision Processes (MDPs) | ||
Line 17: | Line 19: | ||
---- | ---- | ||
- | ===== Properties supported by ePMC ===== | + | ===== Properties supported by EPMC ===== |
* PCTL | * PCTL | ||
* PLTL | * PLTL | ||
Line 26: | Line 28: | ||
- | [[https://iscasmc.ios.ac.cn/iscasmcwp/?page_id=370|Example: LTL Pattern Formulas]] | + | We give some example LTL properties which can be specified in EPMC. In our tool, such formulas can be used in form '' |
+ | |||
+ | * Bounded responsibility property, '' | ||
+ | * Bounded responsibility property with fairness, '' | ||
+ | * Bounded responsibility property with fairness, '' | ||
---- | ---- | ||
- | ===== Manual, structure of the tool ===== | + | ===== Manual, structure of the EPMC ===== |
EPMC has three main components: the frontend web interface, the backend for handling requests from the frontend, and the model checker engine. A database engine is used to store information. | EPMC has three main components: the frontend web interface, the backend for handling requests from the frontend, and the model checker engine. A database engine is used to store information. | ||
- | For more details, please visit here: [[https:// | + | |
+ | **The Frontend Web Interface: | ||
+ | |||
+ | After logging into the system, it offers several views, including: | ||
+ | |||
+ | * **Message Centre.** The message centre provides the user recent news. Particularly, | ||
+ | * **Model Centre.** The model management centre lists available models, their type (currently only PRISM models are supported), comments, options, last updated snapshot and all available operations for the model. From the menu above one can also upload or create new models. The properties are associated to models. | ||
+ | * **Task Centre.** In the model centre, the user can choose to check selected properties or all properties. This is referred to as a task. Note that a task is created as a snapshot of the current model, (selected) properties and options. This allows the user to modify the model/ | ||
+ | * **Option Centre.** From the option centre the user can set the user level options. Moreover, for each model to be analysed, one may modify certain options and get model level options. The model level options have higher priority and will overwrite user level options. | ||
+ | * **Example Centre.** From the example centre, the user can directly import several examples together with associated properties into her own account. | ||
+ | |||
+ | **The Interface.** While the frontend does not play a role in the evaluation of the model, it includes a fast syntax check that allows for checking the syntactical correctness of the model while interacting with the editor. | ||
+ | |||
+ | The part available to the frontend is a stand-alone program (on the server side) that makes use of only a small part of the classes in the model checker engine. This lightweight version is only used for checking the syntactical correctness of models from the client side, while the full version on the model checker site also constructs the respective models and automata. These syntactical correctness checks are simple and can thus be done efficiently on-demand, bypassing the scheduling queue. | ||
+ | |||
+ | **The Database**, powered by MySQL(tm), contains all information needed to elaborate the models: besides the user details, it stores the models and the relative properties defined by the user, as well as the tasks the user creates by requiring an operation on the model. Each task is created by the frontend DBMS module as snapshot of the model and the corresponding properties and options, such that it is not affected by subsequent changes. Once a task is completed, it is updated by the backend DBMS module with the evaluation of the properties (or with an error message), according to the model checker outcome. The tasks are kept until the user explicitly removes them via the task centre. | ||
+ | |||
+ | **The Backend.** The main job of the backend is to poll tasks from the database and evaluate them. It currently adopts a FIFO approach to retrieve the tasks from the DBMS module. These tasks are then sent to several instances of EPMC that run in parallel in independent worker threads. Once a worker completes her task, she sends the outcome to the data store, whose main jobs are to keep track of busy workers and to collect the results. Since the evaluation of a task may take some time, the worker periodically sends status updates to the data store. The result collector retrieves the available results from the data store and forwards them to the database via the backend DBMS module. | ||
+ | |||
+ | **The Model Checker Engine.** The model checker is the working horse of the system. Each work thread will parse and translate the model and the specification it is going to be checked against. For complex LTL subformulas (that is, for each linear part φ of PCTL* outside of the simple PCTL operators), we first use SPOT to generate the generalised Büchi automaton. Unless this is already deterministic, | ||
---- | ---- | ||
===== Access to EPMC ===== | ===== Access to EPMC ===== | ||
* Download: EPMC is now available publicly. It can be obtained on GitHub, at [[https:// | * Download: EPMC is now available publicly. It can be obtained on GitHub, at [[https:// | ||
- | * Online version of EPMC is available [[https://iscasmc.ios.ac.cn/ | + | * Online version of EPMC is available [[https://tis.ios.ac.cn/ |
{{: | {{: | ||
Line 54: | Line 79: | ||
=== How to install and use === | === How to install and use === | ||
- | This tool is implemented as a plugin in ePMC. The source code can be found at https:// | + | This tool is implemented as a plugin in ePMC. The source code can be found at https:// |
To perform PETL model checking, please set the following options: | To perform PETL model checking, please set the following options: | ||
Line 72: | Line 97: | ||
You need to prepare 3 files: one for the model, one for equivalence relations, and one for properties. | You need to prepare 3 files: one for the model, one for equivalence relations, and one for properties. | ||
- | The models should be in the PRISM format([[http:// | + | The models should be in [[http:// |
The equivalence relations are described in this format: | The equivalence relations are described in this format: | ||
Line 100: | Line 125: | ||
</ | </ | ||
- | Other properties can be described by the PRISM language([[http:// | + | Other properties can be described by [[http:// |
==== Plugin: dpCTL ==== | ==== Plugin: dpCTL ==== | ||
=== Introduction === | === Introduction === | ||
Differential privacy is a framework for designing and analyzing privacy measures, which has become a gold standard in data privacy. In this tool, the branching time temporal logic dpCTL is developed for specifying differential privacy. Several differentially private mechanisms are formalized as Markov chains or Markov decision processes. Using formal models, subtle privacy conditions are specified by dpCTL. In order to verify privacy properties automatically, | Differential privacy is a framework for designing and analyzing privacy measures, which has become a gold standard in data privacy. In this tool, the branching time temporal logic dpCTL is developed for specifying differential privacy. Several differentially private mechanisms are formalized as Markov chains or Markov decision processes. Using formal models, subtle privacy conditions are specified by dpCTL. In order to verify privacy properties automatically, | ||
- | Our tool is built as a plugin of the model checker | + | Our tool is built as a plugin of the model checker |
---- | ---- | ||
+ | ====== Case Studies ====== | ||
+ | We have successfully analysed several case studies. Most of them are taken from the [[http:// | ||
+ | * [[http:// | ||
+ | * [[http:// | ||
+ | * [[http:// | ||
+ | * [[http:// | ||
+ | * [[http:// | ||
+ | * [[http:// | ||
+ | ---- | ||
====== Other projects ======= | ====== Other projects ======= | ||
- | The following are projects related to ePMC: | + | The following are projects related to EPMC: |
* [[http:// | * [[http:// | ||
+ | * [[https:// | ||
* [[https:// | * [[https:// | ||
main.1614305165.txt.gz · Last modified: 2021/02/26 10:06 by merlin