Extending a User Interface Prototyping Tool with Automatic MISRA C Code Generation

TL;DR

This paper presents a tool that automatically generates MISRA C code from formal user interface models, enhancing safety-critical system development like medical devices.

Contribution

It extends the PVSio-web prototyping toolkit to produce verified MISRA C code, bridging formal models and implementation for safety-critical applications.

Findings

Successfully generated MISRA C code for a medical device interface

Validated the approach with a real-world data entry system

Demonstrated potential for improving safety and reliability in user interface development

Abstract

We are concerned with systems, particularly safety-critical systems, that involve interaction between users and devices, such as the user interface of medical devices. We therefore developed a MISRA C code generator for formal models expressed in the PVSio-web prototyping toolkit. PVSio-web allows developers to rapidly generate realistic interactive prototypes for verifying usability and safety requirements in human-machine interfaces. The visual appearance of the prototypes is based on a picture of a physical device, and the behaviour of the prototype is defined by an executable formal model. Our approach transforms the PVSio-web prototyping tool into a model-based engineering toolkit that, starting from a formally verified user interface design model, will produce MISRA C code that can be compiled and linked into a final product. An initial validation of our tool is presented for the data entry system of an actual medical device.

Figures

Tables

Table 1. Table 1: Structure of a header file. Non-terminal symbols are enclosed between angle brackets; square brackets enclose optional symbols.

$⟨$ headerfile $⟩$	::=	$⟨$ preprocessor_directives $⟩$
		[ $⟨$ constant_definitions $⟩$ ]
		$⟨$ typedef_definitions $⟩$
		$⟨$ state_labels_enum $⟩$
		$⟨$ state_structure $⟩$
		$⟨$ utility_functions $⟩$
		$⟨$ init_function $⟩$
		$⟨$ permission_functions $⟩$
		$⟨$ transition_functions $⟩$

Equations

$$\mathbf{arc}\frac{ϵ,(p,q,e,g,v^{\prime });ϵ=e\wedge n=p\wedge v\models g}{⟨n,v⟩\to ⟨q,v^{\prime }⟩}$$

$$\mathbf{idle}\frac{ϵ,(p,q,e,g,v^{\prime });ϵ\ne e\vee n\ne p\vee v/\models g}{⟨n,v⟩\to ⟨n,v⟩}$$

$${\mathbf{arc}}_P\frac{ϵ,(p,q,e,g,v_c^{\prime });ϵ=e\wedge v_n(x_{\mathrm{curr}})=p\wedge v_c\models g}{⟨v_n,v_c⟩\stackrel{P}{⟶}⟨q,v^{\prime }⟩}$$

$${\mathbf{idle}}_P\frac{ϵ,(p,q,e,g,v_c^{\prime });ϵ\ne e\vee v_n(x_{\mathrm{curr}})\ne p\vee v_c/\models g}{⟨v_n,v_c⟩\stackrel{P}{⟶}⟨n,v_c⟩}$$

Full text

1 Introduction

Formal methods are important for developing and understanding safe and secure systems. The PVSio-web framework [21, 22, 23, 27] allows developers to use formal methods in a friendly and appealing way as it provides realistic animations and is integrated with a graphical editor for the Emucharts language [24]. (Emucharts is a state machine formalism with guards and actions associated with transitions; it is explained further in Sect. 3.4 below.)

PVSio-web uses the formal modelling language of the Prototype Verification System (PVS) [28], including the PVSio extension [25]. PVS is an industrial-strength theorem proving system that allows formal verification of safety and reliability properties of hardware and software systems [6, 32]. Although PVS itself is very effective, it is not widely used for model-based development and analysis of user interfaces, as the tool has a steep learning curve. PVSio-web softens this learning curve, making the tool more user-friendly and accessible, providing developers with a graphical modelling environment, and a toolbox for developing realistic visual prototypes of user interfaces.

The applications of embedded software in safety-critical applications increase continuously. Taking this into account, together with the requirements to reduce time and overall production costs, automatic code generation plays an essential role. Automatic code generation guarantees a smooth conversion from model to code and reduces the debugging and testing required for source code, provided that the correctness of code generation and of the high-level model have been verified.

We therefore present an extension to PVSio-web that generates C code. Specifically, our extension generates MISRA C [2], a safety-oriented subset of C developed by the Motor Industry Software Reliability Association (MISRA). MISRA C is commonly used in safety-critical subsystems, such as car braking in automotive systems.

With this new extension, formal PVS specifications generated from Emucharts diagrams are automatically converted to C, significantly shortening project development time. Because of the approach, the semantics of generated C code is equivalent to the formal models, and therefore the code retains the reliability and safety properties formally verified for the PVS model.

In summary, our main contribution is an approach to software development that integrates logic- and state machine-based formal modelling, validation by simulation, and automatic implementation by generating production code to be run on the actual system hardware, all based on an industrial-strength formal methods toolkit.

2 Related work

Model-based approaches are commonly used in the field of human computer interaction, for example [14]. Most approaches are focused on describing user interfaces and their implementations at various levels of abstraction. Developers of user interfaces for interactive systems also have to address heterogeneity and adaptation to the context of use. For example, in [30], a model-based declarative language for the design of interactive applications based on Web services in ubiquitous environments was presented. In contrast to these familiar approaches, the present work proposes a framework enabling a formal verification of user interaction. The framework is meant for safety analysis of safety-critical devices and not with user interface design issues as discussed in [30],

Similarly to our approach, formal models were used in [7] to describe functionality and component interactions, where they were combined with user interface models in order to get the entire model of the system. Moreover, an Android emulator application was generated, using Java and XML technologies. Presentation models and presentation interaction models were used in [10] to model interactive software systems; these models were shown to be usable with a formal specification of the system functionality. In [8] the same formalisms were used to model user manuals of modal medical devices, proving that the user manual may be not always consistent with actual device behaviour.

In [18], model checking was used to model and prove properties of specifications of interactive systems so that possibly unexpected consequences of interface mode changes can be checked early in the design process. In [20], the complementary role of model checking and theorem proving in the analysis of interactive devices was considered. Recent work [17] explored the paths that a user will take in interacting with medical devices for the analysis of properties of the behaviour of safety-critical devices. A model-checking approach has also been used to analyse hardware behaviour [5].

A discussion of production code generation in model-based development can be found in [12]. Many papers deal with specific code generators, for example TargetLink [4]. Code generators specifically designed for medical systems are described in [3] and [29].

3 PVS, model-driven development and Emucharts

This section provides background information on the PVSio-web framework and its relationship to model-driven development.

3.1 PVS, the Prototype Verification System

The PVS is an interactive theorem prover for a typed higher-order logic language, providing an extensive set of inference rules based on the sequent calculus [31]. Its PVSio extension is a ground evaluator that can compute the results of ground function applications, that is PVS expressions consisting of a function name applied to variable-free arguments. PVS functions are purely declarative definitions of mathematical mappings, without any procedural information on how to compute them, but the PVSio package can derive and execute an algorithm to evaluate a ground function application, turning it into a procedure call. The PVSio package also provides functions with side effects, such as input and output, which do not interfere with the semantics of a theory.

A system is modelled in PVS as a theory, a collection of logical statements and definitions about the structural and behavioural aspects of the system. The system’s required properties are expressed as theorems to be verified with the PVS theorem prover. If the behavioural aspects are expressed as functions, the system can also be simulated with the PVSio extension. The same logical model can then be used both for verification and simulation.

3.2 Model-driven development

Model-driven development (MDD) is based on creating an executable system model by assembling functional blocks. An executable model makes it possible both to simulate the system and to generate production software to control it. Together with the naturalness of the graphic language of functional blocks, these features make MDD very attractive to developers. However, this approach has two limits: first, functional blocks lend themselves to building design models, but not specification ones; and secondly, formal verification of a block-based model is tedious, and in fact it is uncommon in industrial practice.

A formal approach can be used to create both specification and design models and intrinsically lends itself to rigorous verification of system properties. In particular, logic specification languages, such as PVS, are supported by automatic or interactive theorem provers used by developers to check if system requirements, expressed as logical formulas, are implied by a system’s description expressed in a logic theory. However, formal methods require expertise in languages and methods that are not widely known in the wider developer community. Further, most formal languages abstract from the familiar procedure-oriented computation model of popular programming languages, making it harder to generate executable software.

It is then desirable to have tools and methods providing developers with the features of both approaches. The present work is part of a research effort aimed at this goal. With the PVSio-web framework, a developer can build a model in a graphical state-machine language or a logic language, or both (Sect. 3). The graphical model is translated into the logic language automatically, and the resulting translation is both verifiable and executable using the PVSio ground evaluator, which acts as an interpreter for the PVS language. The PVSio-web framework thus provides features of the formal approach: A formal specification language and a verification tool, and features of MDD, thus providing a full graphical modelling language and a simulation engine. A translator from Emucharts to C makes it possible to generate code from a state machine-based model that can be validated by simulation and verified by theorem proving. The other important feature of MDD — generation of production code capable to be run on the actual system hardware — is a key contribution of this paper.

3.3 PVSio-web

The PVSio-web framework is a set of tools, co-ordinated by a web-based interface, for prototyping and simulation of interactive devices. Its main components are, besides PVS with its PVSio extension: (i) the Prototype Builder, a graphical tool used to choose a picture of an existing or anticipated device’s front panel and to associate PVS functions with active areas of the picture representing device inputs (e.g., buttons or keys) and outputs (e.g., alphanumeric displays or lights); (ii) the Model Editor, a textual interface to write PVS code; (iii) the Emucharts Editor, a graphical tool to draw Emucharts state machine diagrams; (iv) a Simulation Environment; and (v) Code Generators for PVS and other formal languages (currently Presentation Interaction Models [9], Modal Action Logic [16], and Vienna Development Method [13]) — and for MISRA C, as presented in this paper.

PVSio-web can be used to prototype a new device interface, or to create a reverse-engineered model of an existing one. In either case, a developer creates formal descriptions of the device’s responses to user actions, using the model and Emucharts editors, and associates these descriptions with the active areas of the simulated interface, using the prototype builder. In the simulation environment, the developer, or a domain expert or a potential user, interacts with the prototype clicking on the input widgets. These actions are translated to PVS function calls executed by the PVSio interpreter.

3.4 Emucharts

An Emucharts diagram is the representation of an extended state machine in the form of a directed graph composed of labelled nodes and transitions. Transitions are labelled with triples of the form $\mathit{trigger}[\mathit{guard}]\{\mathit{action}\}$, where trigger is the name of an event, guard is an enabling Boolean expression, and action is a set of assignments to typed variables declared in the state machine’s context. The default guard is the true value and the default action is a no-operation. The state of the machine is defined by the current node and the current values of the context variables.

The code generator for PVS produces a theory containing functions that define the state machine behaviour on the occurrence of trigger events. Since an Emucharts diagram usually represents a device response to user actions, such events represent user actions, such as pressing a button on a control panel. During simulation on a PC, a user click on an active area of the device picture causes the simulator to generate a function application expression that is passed to the PVSio ground evaluator.

4 From Emucharts to safe C

The aim of programming code generation in the PVSio-web framework is producing a module that implements the user interface of a device, which can be compiled and linked into the device software without any particular assumptions on its architecture. In this way, the user interface module can be used without forcing design choices on the rest of the software. In our approach, the generated module contains a set of C functions. The main ones are, for each Emucharts trigger: (i) a permission function, to check if the trigger event is permitted, i.e., whether it is associated with any transition from the current state, and (ii) a transition function that, according to the current state, updates it, provided that the guard condition of an outgoing transition holds. The code includes logically redundant tests (assert macros) to improve robustness.

To generate production-quality code fit for safety-critical applications we adopt MISRA guidelines. The MISRA guidelines for the C language, originally conceived for the automotive industry, enforce programming practices to improve maintainability and portability and, above all, to reduce the risk of malfunction due to implementation- or platform-dependent aspects of the C language. For instance, there are rules that bar the use of constructs such as goto, and rules requiring that numeric literals be suffixed to indicate their type explicitly. The generated code currently complies with the first version of the 1998 MISRA C guidelines.

4.1 Code generation

Our MISRA C code generator was implemented in JavaScript using Handlebars [15], a macro-expansion tool for web applications. A Handlebars template is a piece of text containing “Handlebar expressions,” which refer to elements of the surrounding context, typically an HTML document. A Handlebars expression specifies a character string as a function of context elements, which is compiled into a JavaScript function that returns the template text with the substitutions computed by the Handlebars expressions. For example, a template fragment for a C preprocessor #include directive is #include "{{filename}}.h", where the Handlebars expression {{filename}} contains the filename parameter that will be replaced by the actual name of the file to be included.

The code generator produces a header file, an implementation file, a makefile, a simple test driver file, and a documentation manual.

The structure of the header file is defined by the grammar in Table 1. The header file contains, among other items, the declarations (typedef_definitions in the grammar) for types with explicit representation of size and sign, e.g., UC_8, for eight-bit unsigned char, the declaration (state_labels_enum) for an enumeration type defining the node labels, and the declaration (state_structure) for the state structure type representing the state of the Emucharts model. This structure contains one context field for each variable defined in the Emucharts context, and two more fields (curr_node and prev_node) contain the labels of the current and the previous node.

The declarations are followed by the function prototypes of the two utility functions enter and leave, the init function, and, for each trigger, one permission and one transition function. The functions receive a pointer to a structure of type state passed by a calling program. The enter and leave functions, called by the init and transition functions, update the curr_node and prev_node fields, respectively, with the target and source node label of the executed transition. The leave function has been introduced to allow future versions to implement checkpointing algorithms. The init function initialises the state’s context fields with the values of the context variables specified in the Emucharts diagram, and the curr_node field with the label of the initial node. As mentioned above, each permission function checks if the current node has a transition labelled by the respective event. Then, the matching transition function chooses among the transitions triggered by that event, according to the respective guards (assumed to be mutually exclusive).

The implementation file contains the function definitions. For example, consider the Emucharts diagram of the data entry system of the Medtronic MiniMed 530G System shown in Figure 3. The diagram has a context variable display of type double represented on 64 bits, which holds the value shown on the device’s display. The node labels and the state type are defined as

typedef enum { off, on } node_label; typedef struct { D_64 display; node_label curr_node; node_label prev_node; } state;

The code for the permission function associated with the click_UP trigger is

UC_8 per_click_UP(const state* st) { if (st->current_state == on) { return true; } return false; }

where the return type UC_8 (eight-bit unsigned character) is used to represent the Boolean type. The transition function is

state click_UP(state* st) { assert(st->current_state == on); assert(st->display < 10 || st->display == 10); if (st->display < 10 && st->current_state == on) { leave(on, st); st->display = st->display + 0.1f; enter(on, st); assert(st->current_state == on); return *st; } if (st->display == 10 && st->current_state == on) { leave(on, st); st->display = 10.0f; enter(on, st); assert(st->current_state == on); return *st; } return *st; }

A proof of the correctness of this translation schema is shown in Appendix A.

5 Case study

The Alaris GP, made by Becton Dickinson and Company, was used as a case study for the MISRA C code generator.

This volumetric infusion pump is a medical device used for controlled automatic delivery of fluid medication or blood transfusion to patients, with an infusion rate range between 1 ml/h and 1200 ml/h. It has a monochrome dot matrix display with three significant digits, and has 14 buttons for operating the device (see Figure 4). The pump has a rather complex user interface, with different modes of operation and ways of entering data, including the possibility of choosing from a list of preloaded treatments. For simplicity, in this paper only the essential part of the data entry interface, concerning numerical input and display, is considered.

Numerical input is done through the chevrons buttons: upward and downward chevrons increase and decrease, respectively, the displayed value. The amount by which the value is increased or decreased depends on whether a single or double chevron is pressed, and on the current displayed value. More precisely, the displayed value is changed as follows: (i) If the displayed value is below $100$, the value changes by $0.1$ units for a single chevron, and steps up or down to the next decade for a double chevron (e.g., from $9.1$ to $10.0$); (ii) if the displayed value is between $100$ and $1,000$, the value changes by $1$ unit for a single chevron, and steps up or down to a value equal to the next hundred plus the decade of the displayed value for a double chevron (e.g., from $310$ or $315$ to $410$); (iii) if the displayed value is $1,000$ or above, the value changes by $10$ units for a single chevron, and steps up or down to a value equal to the next hundred for a double chevron (e.g., from $1,010$ or $1,080$ to $1,100$).

The Emucharts diagram for the numeric data entry is shown in Fig. 5. Triggers click_alaris_up and click_alaris_dn represent clicks on the upward and downward single-chevron buttons, respectively, and triggers click_alaris_UP and click_alaris_DN represent clicks on the double-chevron ones. For each event, combinations of guards and actions specify the rules described above.

The PVS code generator translates the diagram into an executable logic theory, and the C code generator produces permission and transition functions for each trigger, as explained previously.

5.1 Mobile applications

The PVSio-web framework uses a standard web interface to integrate its tools: this approach offers a uniform interface that a developer can access with any web browser.

Our framework has been extended by providing the possibility to run simulations on a mobile device. Smartphones and tablets improve usability and help make user interaction similar to actual device operation. For example, mobile devices could be used in a hospital environment to train medical personnel and patients.

An interactive device can be simulated using the C source code produced by the PVSio-web generator, compiled and linked with a mobile device-specific application. For example, the code for the user interface of the Alaris infusion pump has been ported to the Android [11] platform using the Android NDK [26] toolset, which can embed C code in a Java project, relying on the Java Native Interface (JNI) [19].

6 Conclusions

We presented the implementation of our MISRA C code generator for the PVSio-web prototyping toolkit. Automatic code generation significantly reduces project development time. Our approach eliminates a human-performed step in the development process: user interface software engineers no longer need to convert the design specifications into executable target code.

Our tool improves the development of safe and dependable user interfaces, as it greatly facilitates using formal methods easily and reliably with real UIs, which we demonstrated with the medical device examples in this paper.

Current and future directions include improving this initial integration with other features of C, still conformant to MISRA C under the most recent 2012 rules. We plan to develop code generators for programming languages such as C++, Java and ADA.

Acknowledgements

This work was partially supported by the PRA 2016 project “Analysis of Sensory Data: from Traditional Sensors to Social Sensors” funded by the University of Pisa.

Appendix A Correctness of code generation

In order to assess the correctness of the generated code, the Emucharts diagram is taken as the reference model, and a correspondence is established between the evolution of the model and that of the executed code.

A.1 Transition system for an Emucharts diagram

As discussed above (section 4), an Emucharts diagram is a graph of nodes and labelled transitions, extended with a set of typed context variables, each one with an initial value. Its semantics is given by a transition system. Let the following be defined:

• •

A set $N=\{n_{1},\ldots,n_{i}\}$ of nodes;

• •

a set $X=\{x_{1},\ldots,x_{j}\}$ of context variables (for simplicity, assumed to be typeless);

• •

a set $\mathbb{V}$ of values;

• •

a set $E=\{\epsilon_{1},\ldots,\epsilon_{k}\}$ of events;

• •

a set $G=\{g_{1},\ldots,g_{l}\}$ of guards, i.e., Boolean expressions involving variables, constants from $\mathbb{V}$, arithmetic and relational operators;

• •

a denumerable set $V$ of valuations, i.e., functions from $X$ to $\mathbb{V}$;

• •

a set $A=\{a_{1},\ldots,a_{l}\}$ of arcs, i.e., 5-tuples of the form $(s,t,e,g,v)$, where $s,t\in N$ are the arc’s source and target node, $e\in E$, $g\in G$, and $v\in V$ is the valuation defined by the action labelling the corresponding transition in the diagram; more precisely, $v$ is the valuation obtained by overriding the previous valuation with the assignments in the action associated with the arc;

• •

a set $\mathbb{Q}$ of states of the form $\langle n,v\rangle$, with $n\in N$ and $v\in V$;

• •

a transition relation ${\rightarrow}\subseteq Q\times Q$, defined by the semantic rules in Figure 6, where the premises contain an event $\epsilon$, an arc label, and a logical condition, and the consequences contain a member of the transition relation that is enabled if the condition holds.

With the above definitions, the associated transition system $T$ is the tuple $(\mathbb{Q},\rightarrow,q_{0})$, where $q_{0}=\langle n_{0},v_{0}\rangle$ is the initial state. Since the diagram is deterministic, given a sequence of event occurrences $e_{1},~{}\ldots,e_{k},~{}\ldots$, the transition system has only one sequential path. If an event cannot affect a state (either it is not permitted or no guard prefixed by the event is satisfied), the system does not change state. The operational semantics are given in Figure 6.

A.2 Transition system for the generated code

The generated functions are used within a more complex system, which is responsible for catching events at the real or simulated user interface and for calling the respective functions according to an appropriate protocol: the init function must have been called previously, then, when an event is catched, the permission function of the corresponding trigger is called, and only if it returns true can the respective transition function be executed.

Assume that the data entry subsystem of the device is controlled by a program $P$ that responds to input events by calling the respective functions. These function will take the device to the next state.

Also the program $P$ can be modelled as a transition system $T_{P}$ based on the following sets, each one being isomorphic ($\cong$) to the corresponding set in $T$, or an extension to that set: (i) A set $N_{P}\cong N$ of node labels, each represented by an enumerator of the node_label type in $P$; (ii) a set $X_{P}=X_{c}\cup\{x_{\mathrm{curr}}\}$ of variables, where $X_{c}\cong X$, each variable in $X_{c}$ represents a context field of the state structure in $P$, and $x_{\mathrm{curr}}$ represents the curr_node of the state structure; (iii) a set $\mathbb{V}_{P}=\mathbb{V}_{c}\cup N_{P}$ of values, where $\mathbb{V}_{c}=\mathbb{V}$; (iv) a set $E_{P}\cong E$ of events, each one associated with one permission function and one transition function in $P$; (v) a set $G_{P}\cong G$ of guards, each implemented as the condition of an if statement in $P$; (vi) a denumerable set $V_{P}=V_{c}\cup V_{n}$ of valuations from $X_{P}$ to $\mathbb{V}_{P}$, where $V_{c}\cong V$ and $V_{n}\colon\{x_{\mathrm{curr}}\}\rightarrow N_{P}$; (vii) a set $A_{P}\cong A$ of arcs, where each arc has the form $(v_{n}(x_{\mathrm{curr}}),v^{\prime}_{n}(x_{\mathrm{curr}}),e,g,v^{\prime}_{c})$, and each arc represents an if statement in the transition function for event $e$ having guard $g$ as its condition and valuation $v^{\prime}=v^{\prime}_{n}\cup v^{\prime}_{c}$ as its controlled statement, with $v^{\prime}_{n}$ implemented by the enter function and $v^{\prime}_{c}$ by the assignments specified in the Emucharts diagram.

With the above definitions, let $Q_{P}$ be a set of states where each state is a pair $\langle v_{n},v_{c}\rangle$, with $v_{n}\in V_{n}$, $v_{c}\in V_{c}$. The transition relation ${{\overset{P}{\longrightarrow}}}\subseteq Q_{P}\times Q_{P}$ is defined by the semantic rules in figure 7 applied to elements of the above sets, and implemented by the permission functions, which check for each event $e$ if the condition $v_{n}(x_{\mathrm{curr}})=p$ holds or not, and by the transition functions, which check if the current values of the variables satisfy the guards, and update node and variables accordingly. The associated transition system $T_{P}$ is the tuple $(Q_{P},{\overset{P}{\longrightarrow}},q_{P0})$, where $q_{P0}$ is the state defined by the initial values of $x_{\mathrm{curr}}$ and of the context variables, set by the init function. The operational semantics are given in Fig. 7.

A.3 Equivalence of the transition systems

To prove the correctness of the generated code, we introduce the definition of equivalence between Emucharts states and the program states.

Definition 1.* A member $m$ of one of the sets $N$, $X$, $\mathbb{V}$, $E$, defined in $T$, is equivalent ($\sim$) to the member $m_{P}$ paired to $m$ by the isomorphism between the set containing $m$ and the corresponding set in $T_{P}$.*

Definition 2.* A state $q=\langle n,v\rangle$, $q\in Q$, is equivalent ($\sim$) to a state $q_{P}=\langle v_{n},v_{c}\rangle$, $q_{P}\in Q_{P}$ iff $n\sim v_{n}(x_{\mathrm{curr}})$ — so the value of $x_{\mathrm{curr}}$ is equivalent to node $n$, and $\forall_{x\in X}v(x)=v_{c}(x_{P})$ (i.e., matching variables in $q$ and $q_{P}$ have the same values).*

The proof of correctness for the generated code is by induction on the length of computation. We assume that $T$ and $T_{P}$ are the transition systems modelling, respectively, an Emucharts diagram and a program that uses the generated code, respecting the previously introduced protocol, and accepts a sequence of input events.

Theorem 1.* Let $T$ and $T_{P}$ be the transition systems introduced in the above paragraphs, and $e=e_{1},e_{2}\ldots$ be a sequence of input event sequences. Let $\sigma=q_{0},q_{1},\ldots$ and $\sigma_{P}=q_{P0},q_{P1},\ldots$ be sequences of states, with $q_{i}\rightarrow q_{(i+1)}$ and $q_{Pi}{\overset{P}{\longrightarrow}}q_{P(i+1)}$.*

We prove that, at each step of the computation, $q_{i}\sim q_{Pi}$:

Induction base. $q_{0}\sim q_{P0}$ by construction.

Induction step. Let $q_{j}\sim q_{Pj}$ at step $j$. On the occurrence of an event $e$, let $q_{j}\rightarrow q_{(j+1)}$ and $q_{Pj}{\overset{P}{\longrightarrow}}q_{P(j+1)}$. We can prove that $q_{(j+1)}\sim q_{P(j+1)}$ by case analysis: (1) $e$ not permitted in $q_{j}$; (2) $e$ permitted and guard not satisfied; and (3) $e$ permitted and guard satisfied.

Case 1: $e$ not permitted. If the event is not permitted in the current state, rules $\mathbf{idle}$ and $\mathbf{idle}_{P}$ apply to $T$ and $T_{P}$, respectively, so that $q_{(j+1)}=q_{j}$ and $q_{P(j+1)}=q_{Pj}$, equivalent by induction hypothesis. Recall that the permission function for $e$ returns false in this case, and by hypothesis program $P$ does not call the corresponding transition function.

Case 2: $e$ permitted and guard not satisfied. Also in this case, rules idle and $\mathbf{idle}_{P}$ apply to the transition systems. The if statements in $P$ check that the guard does not hold, and the respective controlled statements are not executed.

Case 3: $e$ permitted and guard satisfied. In this case, Rules arc and $\mathbf{arc}_{P}$ apply to both transition systems, therefore (i) $T$ moves from state $q_{j}=\langle n,v\rangle$ to state $q_{(j+1)}=\langle n^{\prime},v^{\prime}\rangle$, or (ii) $T_{P}$ moves from state $q_{Pj}=\langle v_{n},v_{c}\rangle$ to state $q_{P(j+1)}=\langle v^{\prime}_{n},v^{\prime}_{c}\rangle$. Valuation $v^{\prime}_{n}$ maps $x_{\mathrm{curr}}$ to a node label equivalent by definition to $n^{\prime}$, and $v^{\prime}_{c}$ maps the context variables in $T_{P}$ to values equivalent by definition to those assigned by $v^{\prime}$ to the context variables in $T^{\prime}$.

The new states in the two transition systems are therefore equivalent.