19 July 2016 at Newcastle University, Newcastle upon Tyne, UK

A large number of models that are employed in the field of concurrent systems' design, such as Petri nets, Signal Transition Graphs, gate-level circuits, dataflow structures – all have an underlying static graph structure. Their semantics, however, is defined using additional entities, e.g. tokens or node/arc states, which collectively form the overall state of the system. We jointly refer to such formalisms as Interpreted Graph Models (IGMs).

Workcraft is flexible framework for development of IGMs. It provides a graphical frontend for capturing, (co-)simulation and analysis of IGMs and relies on a number of established backend tools for model checking, synthesis, and verification tasks (Petrify, Punf, Mpsat, etc).

The aim of this tutorial is to overview several IGMs and demonstrate their use to formal modelling and verification of systems and processes from different application domains, such as:

• Signal Transition Graph (STG) and Digital Circuit models will be used for synthesis and verification of asynchronous controllers.
• Dataflow Structures (DFS) formalism will be used for modelling circuit pipelines, analysing their performance and identifying bottlenecks.
• Structured Occurrence Net (SON) model will be employed for investigation of crime and accident scenes.

• Lecture (30 min)
  • Overview of Workcraft framework
  • Supported IGMs and interaction between them

• Morning practical – User interface and basic functionality (90 min)
  • Modelling concurrent vending machine
  • Dining philosophers problem

• Lunch and Learn (90 min)
  • Carving the Perfect Engineer, by Ian Phillips

• Afternoon practical – Design of asynchronous circuits (4 hours)
  • C-element (basic circuit, detailed explanation)
  • Buck controller (medium complexity with some hints)
  • VME bus controller (advanced material for individual work)
  • Analysis and optimisation of asynchronous pipelines

• Demonstration – Applications outside electronics (60 min)
  • Investigation of crime and accident scenes
  • Modelling biological systems

• lecture-introduction_to_workcraft.pdf (907 KiB)
• practical_0-workcraft_overview.pdf (515 KiB)
• practical_1-concurrent_vending_machine.pdf (387 KiB)
• practical_2-dining_philosophers_problem.pdf (546 KiB)
• practical_3-c_element.pdf (557 KiB)
• practical_4-buck_controller.pdf (765 KiB)
• practical_5-vme_bus_controller.pdf (697 KiB)
• practical_6-optimisation_of_asynchronous_pipelines.pdf (537 KiB)