Demo: A Design Studio for Verification Tools

It is often the case that analysis, simulation and verification tools from different sources share a lot of commonalities. Even though the syntax might differ, the semantics of the input models are many times the same. Theoretically this means that different tools could either be compared or combined to analyze different aspects of the same model. In practise however, this often leads to time-consuming manual tweaks and modifications on a per model basis. Additionally, the necessary environments, in form of run-times and dependencies required for the tools to be executed, are not always readily available. Images for virtual machines and containers surely ease the process for setting up the context, but this still requires manual plumbing when setting up a work-flow. In this demo a Design Studio for combining different verification tools is show-cased. Building on top of WebGME (Generic Modeling Environment) it provides end-users with an online, browser-based editor where models are stored in a version-controlled, centralized database. At any point of the design process, a model can at the click of a button be requested to act as input for a range of different verification tools such as SpaceEx, Flow* and dReach. The Design Studio is currently hosted at cps-vo.org, but also available as open source and the entire system can, thanks to containerization, be hosted locally with a single command. At the core of this Design Studio lies the HYbrid Source Transformer, HYST, which is hosted as an independent service for translating a common model format, SpaceEx, into each tool-specific format.