Verifying Petri Net-Based Models of Agent-Oriented Software Engineering

1. 2. Transform ERS to PT net

1.1. Establish a set of transformation rules from ERS into P/T nets

1.2. Show isomorphism of the state spaces

1.3. analyse the computational complexity

2. 3. Implemented proposed rules as a computer program called ERStoPTnet

2.1. Draw ERS in Renew and Export its PNML

2.2. Import PNML into Java (Eclipse)

2.3. Automatically compute transformation Algorithm to obtain PT-net

2.3.1. output PT-net PNML for export to Renew

2.3.2. output textual PT-net representation that PUNF requires

3. 5. Input PT-net textual representation into PUNF

3.1. Output complete finite prefix of unfoldings of the transformed ERS

4. 1. Modify Elementary Object System

4.1. Assign names to object nets

4.2. Eliminate typing of system net places

4.3. Assign variables to system net arcs

4.4. Define Elementary Reference-net System (ERS)

4.5. Impose structural restrictions

4.6. Impose dynamic restrictions

5. 6. Encode into CNF the reachability and deadlock-freeness problems

5.1. Model check CNF using SAT solver

6. 7. Perform comparative analysis with existing result on benchmark models

7. 4. Import PNML representation of PT-net into Renew to show prove of concept

7.1. Output simulation result