The goal of this method is to guide the model checking process of many variations of similar specifications of Real Time behaviour, using an intermediate set of configuration tables to guide the set of variants.

Model checking is a method to verify if a model of the system under verification satisfies its requirements. In complex models verification becomes infeasible due to the large state space, requiring many small variations of the model, one for each set of related requirements. Typically, these variations are built independently, intersecting efforts, and not guaranteeing that they are kept consistent.

This method explores how to define this of variations and respective requirements based on a single configurable model, leveraging on principles from software product line engineering (SPLE), which are here applied to formal specifications rather than software specifications. It focuses on the UPPAAL real-time model checker, and proceeds in two phases: (1) annotation of the specifications, and (2) automatic configuration of these annotated blocks via a product line of specifications.

== 1. Annotated Specifications ==

In many cases the relation between the abstract model and the implementation is maintained via personal meetings and reports using natural languages. Automatizing this synchronisation is involves a large effort and is in many cases impractical. Our approach involves using a set of tables in Microsoft Excel to maintain the key parameters of the formal models, including scenarios and requirements of the system. This set of tables is easy to be read and modified by both developers of the system and by developers of the formal models and is automatically entangled with the models used by the formal analysis tools. On one hand, the system developers can update this table and check which requirements can be verified; on the other hand, the designers of the formal models can adapt the model to either include new details, or to relax aspects that introduce state explosions. By using an intermediate representation of the core parameters of the formal specifications, we reduce the expected knowledge of the system developers over formal models. This includes ranges of estimated time executions of individual components, the number of times certain actions may occur, and sequences of input scenarios. Experts in formal modelling are kept in the loop to refine the models and property specifications as needed.

== 2. Product Line of Specifications ==

A common approach to avoid exploring too many states while trying to verify a property is to bound the state space. Some tools support bounded model checking, limiting the depth of search in the state space. Our approach supports the specification of variants, where the state-space can be reduced by modifying different parameters of the specification. For example, 2 variants could remove 2 independent parts of the specification, allowing the verification of properties for these two variants instead of the full model. Ultimately, the goal is to verify a large-enough set of variants to cover the relevant cases without incurring in state-space explosions. 

The method workflow is as follows. The informal behavioural description, different parameters, input scenarios, and requirements are provided as input. These are used to manually build: (1) an initial global and annotated real-time specification, and (2) a collection of Excel tables with information on how to populate the annotated blocks of the specifications and with the set of requirements. Our own tool (Uppex) is then used to automatically apply the configurations in the Excel tables to the annotated specifications, producing a set of specification instances. These are also automatically analysed via UPPAAL, with a provided time-out, and a report is produced over which requirements hold in which configuration. The instances can also be manually inspected within UPPAAL, leading to a manual refinement of the annotated specifications and the Excel tables, until all desired requirements are met for a rich enough set of configurations.