MIMETIC

Overview

MIMETIC (Model-checking with Independent clocks and Clock Derivatives) is a verification tool designed to model, analyze, and verify Distributed Real-Time Applications (DRTA). It extends traditional Timed Automata and Lv logic with independent clocks and Clock Derivatives (i.e., idTA and DLv logic).

MIMETIC allows users to:

Model: real-time systems with independent clocks and Clock Derivatives.
Verify: complex temporal properties.
Analyze: Protocol scenarios, including FireWire - IEEE 1394 Protocol, Fischer’s Protocol, etc.

Installation

Pre-requisites

Before installing MIMETIC, ensure that your system has the following dependencies installed:

Java 11
Python (version 3.6+)
Maven (for building the project)
ANTLR (ANTLR4)
UPPAAL (optional, for verifying traditional Timed Automata)

Install Required Libraries: First, install the required JARs into your local Maven repository.

Install juppaal.jar in local maven repository:
 bash
    mvn install:install-file -Dfile=juppaal-1.0.2.jar -DgroupId=de.tudarmstadt.es -DartifactId=juppaal -Dversion=1.0.2 -Dpackaging=jar -DgeneratePom=true

 Check if installation was successful in local maven repository /home/user/.m2/repository/de/tudarmstadt/es/ 

 Install ImplThesis.jar file to the local maven repository: 
bash
    mvn install:install-file -Dfile=/path/to/file.jar -DgroupId=com.jortizve7 -DartifactId=implthesis -Dversion=0.0.1 -Dpackaging=jar -DgeneratePom=true

Building and Running MIMETIC

Open the project in IntelliJ (or any Java IDE).

Ensure all Maven dependencies are resolved.

Run the project using any of the provided configurations (GUI or CLI).

Usage Modeling a System

1. Model Input Format (XML): MIMETIC accepts input models in an extended UPPAAL-like XML format, which supports:

   Clock declarations.

   Rate constraints on derivatives (e.g., x' <= 1, x' >= y').

   Standard locations, transitions, and invariants.

   Atomic propositions for verification.

ExampleSys x, y x <= 10 x' = 1 && y' <= x' ... x >= 5 x := 0 ...

3. Specifying Properties in $DL_{\nu}$

Properties are written in the input box or in a .dlv file. Here's an example:

x in EE(x <= 3 && x >= 1 && tt) && (y' >= 1 && tt)

This property expresses:

“There exists an execution where clock x is between 1 and 3 and action a eventually occurs.”

And “clock y progresses at a rate of at least 1 before action b.”

Refer to the provided grammar (Figures 12 and 13 in your manuscript) for the complete syntax of:

rateConstraint

clockConstraint

Modal operators like <a>, [a], EE, AA, in, etc.

Syntax DLv: The syntax of the logic operators is the following one: ∧ is
&&, ∨ is ||, < a > is < a >, [a] is [a], x in is x in, ∃ is < @ >, ∀ is [@]; tt
is true, ff is false.    

4. Run the verification: GUI Mode (Recommended)

   java -cp DMLv.jar:$HOME/.m2/repository/de/tudarmstadt/es/juppaal/1.0.2/juppaal-1.0.2.jar::$HOME/.m2/repository/com/jortizve7/implthesis/0.0.1/implthesis-0.0.1.jar be.unamur.mlvl.entrypoint.Main -gui=true (you can use the GUI and open the model (XML file) in the resources/ folder and write the property)

Features in Development

Graphical User Interface (GUI): A user-friendly GUI to simplify modeling and analysis.

Examples

Please review the resources/ folder for examples (models and formulas).

Grammer MIMETIC

document : automataDeclr logicDeclr ;

automataDeclr : AUTOM ':' ID '[' clocksDeclr locations transitions invariants atomicProps ']' ';' ; clocksDeclr : CLOCKS ':' ID (','ID)* ; locations : LOCATIONS ':' ID (','ID)* ; transitions : transition (','transition)* ; transition : ID '-' ID('!')? (',' clockConstraint)? ',' edge; edge : ('{'ID'}')? '->' ID ; invariants : INVAR ':' ID SAT clockConstraint (',' ID SAT clockConstraint ) ; atomicProps : ATOMIC PROPOSITIONS ':' ID SAT proposition (',' ID SAT proposition)* ; logicDeclr : DECL ID '[' ID SAT proposition ']' ';';

propositions : proposition;

proposition : TOP #tt | BOT #ff | proposition (S|WS)? AND (S|WS)? proposition #conjunction | proposition OR proposition #disjunction | '['ID']' proposition #boxModality | '<'ID'>' (S|WS)? proposition #diamondModality | 'EE''(' proposition ')' #existsModality | 'AA''(' proposition ')' #forallModality | clockFormula (S|WS)? 'in' (S|WS)? proposition #inModality | clockConstraint #clockCC | clockFormula '+' NATURAL comparisonOp clockFormula '+' NATURAL #clockOperation | rateConstraint #rateCC ;

clockConstraint : clockFormula (S|WS)? comparisonOp (S|WS)? NATURAL | clockConstraint (S|WS)? AND (S|WS)? clockConstraint | TOP ;

rateConstraint : ID QUOTE (S|WS)? comparisonOp (S|WS)? NATURAL #constantRC | ID QUOTE (S|WS)? comparisonOp (S|WS)? ID QUOTE #simpleRC | rateConstraint (S|WS)? AND (S|WS)? rateConstraint #conjunctionRC | TOP #trueRC | BOT #falseRC ;

clockFormula: ID ('^' ID)?; comparisonOp: '>' | '<' | '>=' | '<=' | EGA ;

fragment DIGIT : [0-9] ;

QUIT : 'quit' ; AUTOM : 'Automata' ; DECL : 'Declaration' ; FSYNCH : 'Fsynchro' ; TABLE : 'Table' ; SYSTEM : 'System' ; INVAR : 'Invariants' ; CLOCKS : 'Clocks' ; LOCATIONS : 'Locations' ; TRANSITIONS : 'Transitions' ; ATOMIC : 'Atomic' ; PROPOSITIONS: 'Propositions' ; NULL : 'NULL' ; ACTIVITIES : 'Activity' | 'Activities'; IN : 'in'; EXISTS : 'EE'; FORALL : 'AA'; AND : '&&' ; OR : '||' ; NOT : '-' ; TOP : 'tt'; BOT : 'ff' ; ACCOG : '{' ; ACCOD : '}' ; CROG : '[' ; CROD : ']' ; PARG : '(' ; PARD : ')' ; AFF : ':' ; FSEP : ';' ; SEP : ',' ; POINT : '.' ; STAR : '' ; FLECHE : '->'; APPROX : '~' ; SAT : '|='; REC : '?' ; SEN : '!' ; PARAM : '%' ; AROB : '@' ; WITHOUT : '\'; PLUS : '+' ; EUNTIL : '[@)'; IMPL : '=>'; INFE : '<='; INF : '<'; LESS : '<'; SUPE : '>='; SUP : '>'; EGA : '=='; SOUL : '_'; QUOTE : '''; NEGATIVE : '-'DIGIT+; NATURAL : DIGIT+; WEDGE : '^' ; ID : a-zA-Z_ ; //COMMENT : '#'(.)*?'\n' ; WS : [ \t\n]+ ; S : [ \t]+;