Sample Network Input, Generated UPPAAL Models, and Verification Output for the APV Tool

Description: This repository contains a synthetic example illustrating the input, generated formal models, and verification output produced by the APV (Automated Protection system Verification) tool, described in the manuscript "A Formal Verification Framework for Automated Protection System Selectivity in Critical Power Distribution Networks" (Nagy Mansour et al., under review at Electric Power Systems Research). The network used in this example was constructed for illustration purposes and does not represent any real distribution network. Files (9 total): Example_20bus_Network_1.json : Sample network description, in the JSON format used as input to the APV tool. output.log : Unfiltered output produced by the UPPAAL verifier for this network. This is the raw log parsed and filtered by the APV tool to produce the results reported in the paper. Uppaal_code_generation_1.xml through Uppaal_code_generation_6.xml : Six UPPAAL model files, one for each subdivided model produced by the tool's Automatic Subdivision of Queries (ASQ), verified independently. Uppaal_code_generation.xml : A single UPPAAL model containing all verification queries for this network in one file, without ASQ subdivision. APV_JSON_field_reference.txt : A txt file explaining the JSON entries and what they represent. Example_20bus_Network_1.png : The online diagram of the 20Bus example network. Requirements to open and run the verification of the models: Opening the .xml model files and running the verification queries requires UPPAAL 5.0, available at https://uppaal.org/downloads/#uppaal5.0. An academic license is required and can be requested at https://uppaal.veriaal.dk/academic.html.