This P model is a state machine based model that models the auto mode (follow a set of mission waypoints) and the ADS-B mode (avoiding other aircrafts).

For each of the models, it checks a safety and liveness property

• auto mode (waypoint mode):
  • safety: when the MissionComplete event is sent, all waypoints must be visited
  • liveness: the intermediate state should be temporary and the drone should not terminate in them / eventually all waypoints are visited
• ADS-B mode (avoidance mode):
  • safety: every intrusion detected must be accompanied by a manuveuring action.
  • liveness: the mode should not terminate on a manuveuring state (while trying to avoid a collision)

Follow the tutorial on https://p-org.github.io/P/getstarted/install/ to download .NET framework and P tool. In the model grouping project, we use P version 2.0.6.0 and .NET version 7.0.203. Any later versions should be backward compatible.

Clone the GitHub repository by executing the following command.

git clone [email protected]:VUISIS/P-Mode-Grouping.git
cd P-Mode-Grouping/

p compile # compile the PSrc, PSpec and PTst
p check   # model check the P model against the PSpec.
          # the specific spec/property must be declared via assert in PTst

For invoking specific test cases, use the following command

p check -tc <test cases> 

There are 3 possible actions for the test cases, namely, waypoint, avoid and global.

• setup a source state machine (files: Ping.p, Pong.p)
• setup module systems (files: PingModules.p) (i.e. module = { }
• setup test script and test driver (files: TestDriver.p, TestScript.p)

• Error: Failed to get test method '' from assembly 'Hello, Version=1.0.0.0, Culture=neutral, PublicKeyToken=null'

  • reinstall or update the p programming language

• global variable initialized to 0 or -1

  • use different variable names for the variable that is passed in and the global variable.