Rany Kahil

Model-based techniques, in particular the Unified Modeling Language (UML), have found wide adoption in the software industry. Formal methods can produce software which is guaranteed to possess desired properties, this being of particular interest where safety or security are concerned. Formal methods have been used very successfully in certain fields like the railway domain (e.g., the verification of the fully automatic lines of the Paris metro system). However, in the wider software industry the adoption of formal methods has been limited. This thesis is part of an effort to ease the uptake of formal methods by enabling a fully formal use of the UML. In pursuing this goal, we want to follow software engineering best practices such as the don't-repeat-yourself principle and modularity.

To achieve this, we use Institution Theory and the Heterogeneous Toolset (HeTS). Institution Theory is a principled way to relate different formalisms in a modular way. The Heterogeneous Toolset is based on Institution Theory and implements tool reuse across different formalisms. This is the context into which we wish to integrate the UML, by providing institutional semantics and HeTS implementations for the different UML sublanguages. Translations between these UML institutions then give joint semantics. Translations to other established languages implemented in HeTS allow us to borrow their tool-support.

The contributions of this thesis to the effort outlined above consist in the development of languages for UML State Machines and Composite Structures and translations to the existing language Casl. We give an account of our languages and translations in terms of Institution Theory, as well as a prototypical implementation in HeTS. Further, we verify properties based on specifications in our languages to demonstrate the feasibility of our approach. The experiences from our work on institutionalisation, implementation and verification moreover point to several opportunities for future work.

showing their tool-supported process for generating a model of an Automatic Train Supervision system. . . . . . . . . . . . . . . . . . . . . . . 5.5 A metro network layout from [START_REF] Mazzanti | Deadlock avoidance in train scheduling: a model checking approach[END_REF]. . . . . . . . . . . . . . . . . . . . . . . . 5.6 A state transition for the train Green1 from [START_REF] Mazzanti | Deadlock avoidance in train scheduling: a model checking approach[END_REF]. The array G1M is the train's mission. G1P is the train's position, given as an index into the mission. Missions from other trains are mentioned to forbid collisions. SA to SF are train counters for critical sections. The two-dimensional array G1C (an example defined in Fig. 5.8 prescribes how movements of Green1 affect these counters. Each critical section counter also has a prescribed maximum value. . . . . . . . . . . . . . . . . . . . . 5.7 An abstraction rule from [START_REF] Mazzanti | Deadlock avoidance in train scheduling: a model checking approach[END_REF] for detecting deadlocks. For a system with two green trains and two red ones, the abstract name ARRIVED is given to system states where each train's position is the final one in its mission (here 13 for all). . . . . . . 5.8 A definition from [START_REF] Mazzanti | Deadlock avoidance in train scheduling: a model checking approach[END_REF] Model-based techniques are widely used in industrial software engineering. Chief among the languages used is the Unified Modeling Language (UML) [FL08, TTR + 13, WBCW20]. The work presented in this thesis sits at the intersection between model-based software engineering in UML on the one hand and formal specification and verification on the other. It is a contribution to a larger effort to apply software engineering principles, in particular, modularity and the reuse of tools and semantics, to specification and verification, and to make the UML usable in such a context. Figure 1.1 shows a motivating example system specified by three UML diagrams. The so-called Composite Structure diagram at the top shows how the system is a composite of two subsystems, representing an ATM (Automated Teller Machine) and a bank in a typical usage scenario. The behaviour of the subsystems is then specified by the State Machines at the bottom.

The state machines are for a scenario where a user wants to withdraw money from the ATM, which requires entry of a bank card and pin, as well as their verification by the bank. In such a scenario the bank and its customer (the user) have an obvious interest in ensuring that an ATM will only behave as if a bank card had been verified if the bank has actually performed that verification successfully. This thesis builds towards expressing such properties and systems in a way that is both mathematically rigorous and has tool-support in accordance with the above-mentioned software engineering principles. In Sect. 13.2 we are then able to prove the stated safety property over the example from Fig. 1.1.

To the best of our knowledge, existing work on UML verification falls into two categories: On the one hand, there are approaches based on model-checking [START_REF] Clarke | Design and synthesis of synchronization skeletons using branching time temporal logic[END_REF][START_REF] Queille | Specification and verification of concurrent systems in cesar[END_REF], e.g. [SWK + 10, tBGM15]. Model-checking is a technique to establish whether a finite-state system satisfies a temporal logic property. Its advantages include full automation and the generation of counterexamples when a property turns out not to hold. However, the applicability of model-checking is limited in theory by the requirement of a finite state space, in practice by the state space explosion problem, where exponential growth of the state space of concurrent systems can quickly exhaust system resources, although there is a large body of work on mitigating this problem [START_REF] Nejati | Handling state space explosion in component-based software verification: A review[END_REF].

On the other hand, there are approaches that verify UML models using interactive theorem provers, e.g. [KFdB + 05, Grö10, BBK + 04]. These approaches can handle systems with large or even infinite state spaces, but bring with them the cost of a human proof engineer.

We suggest to combine the best aspects of both worlds and apply fully automatic theorem provers to infinite state systems. While acknowledging the well-known limits of possibility and feasibility, we aim to make the fully automatic provers available for such UML verification tasks as they can handle while, at the same time, allowing recourse to interactive techniques where subtasks require them. We want to achieve this without requiring a remodelling of the system for each tool or a reimplementation of each checking or proving technique for UML. To achieve these goals, we work within the verification framework HeTS and its theoretical underpinnings, Institution Theory.

The present work is part of a larger effort to provide semantics and tools for the UML in the context of Institution Theory, as first outlined in the position paper [START_REF] Knapp | Towards an Institutional Framework for Heterogeneous Formal Development in UML -A Position Paper[END_REF]. Earlier work as part of this effort includes [START_REF] Knapp | An Institution for Simple UML State Machines[END_REF] (on State Machines) and [START_REF] Knapp | UML Interactions Meet State Machines -An Institutional Approach[END_REF] (on Interactions). In [START_REF] Rosenberger | Relating UML state machines and interactions in an institutional framework[END_REF] we established that the existing approaches to UML State Machines did not satisfy a fundamental condition of Institution Theory, called the Satisfaction Condition. We then proposed that this could best be remedied by creating a multi-modal logic for requiring the presence or absence of certain transitions. A particular State Machine can then be described by sentences requiring that a transition should be possible if the machine mentions it and impossible otherwise1. Hennicker et al. [START_REF] Hennicker | A Hybrid Dynamic Logic for Event/Data-Based Systems[END_REF] propose a similar approach using a simpler logic for event-data systems, as well as an algorithm for systematically computing the sentence 1.1. Contributions and Publications characterising such a system. Their notion of system can be seen as simple UML State Machines without output events, input queues or data parameters. Here, we extend their approach to allow 1. events with data parameters, 2. output events and 3. the combination of State Machines by means of UML Composite Structures, for which purpose we also introduce communication ports and message queues.

We demonstrate the feasibility of our approach by creating a prototypical implementation, integrated into an existing tool landscape, and by carrying out verification tasks on example machines expressed in our formalisms. We will a more extended overview of our approach in Chapter 6, once we have established some background concepts.

Contributions and Publications

The main contributions of the present work are:

1. the development of two modal logic institutions (EDHML and EDHMLO) for embedding and reasoning about simple UML State Machines (the first lacking output events, the second including them), 2. two embeddings to give semantics to simple UML State Machines in terms of our institutions, 3. the development of an institution for simple UML Composite Structures, 4. the comorphisms from these three institutions to Casl, 5. implementations of our languages and translations in HeTS, 6. demonstration of the feasibility of our approach by verifying simple examples which we adapted from the literature and which contain typical challenges.

The most difficult aspects were, on the one hand, the construction of actual institutions, where translation between different vocabularies preserves meaning in the sense required by Institution Theory2, on the other hand, making the fully automatic provers cope with the inductive reasoning in the presence of many possible axioms from which the prover has to select the relevant ones for each step.

We have published our results in two papers, on which the contribution chapters of this thesis are substantially based: Our work on State Machines without output events, including EDHML and UMLState, was published as [START_REF] Rosenberger | Institution-based Encoding and Verification of Simple UML State Machines in CASL/SPASS[END_REF]. The extension to State Machines with outputs and our work on Composite Structures has been published as [START_REF] Rosenberger | An institutional approach to communicating UML State Machines[END_REF]. This includes EDHMLO, UMLStateO and UMLComp. The results of both papers were obtained in collaboration with our coauthors. Although the delineation of individual contributions in a joint research project is always difficult, we attempt to give an indication thereof at the beginning of each contribution chapter.

Outline of the Remainder of this Thesis

The remainder of this thesis is organised as follows:

In Chapter 2, we give a brief introduction to the UML, including a brief history and the motivations for its creation, a discussion of the model types most relevant for us and an overview of some UML tools. Chapter 3 introduces the notions and notations of Category Theory and Institution Theory which we will be using throughout this thesis. Chapter 4 introduces the specification and proof framework HeTS and its central specification language Casl. In Chapter 5 we discuss existing approaches to the verification of models specified in UML.

In Chapter 6, we then give a bird's eye view of our verification approach and its development, i.e., an overview over the contribution chapters of this thesis aimed at readers familiar with the background chapters. Chapter 7 presents the event/data structures underlying our language UMLState, the institution EDHML and a translation from the former to the latter. Chapter 8 introduces a comorphism (a well-behaved translation between institutions) from EDHML to Casl. In Chapter 9, we prepare the connection of State Machines with Composite Structures by extending EDHML to EDHMLO, which adds output events and a notion of ports. We make corresponding extensions to our surface language (now UMLStateO) and to its embedding into the logic. Chapter 10 then extends the comorphism, so it now goes from EDHMLO to Casl Chapter 11 introduces our notion of Composite Structures (UMLComp) and a comorphism from UMLComp to Casl. In Chapter 12, we discuss the implementation of our languages and translations in the context of the Heterogeneous Toolset (HeTS). Chapter 13 contains exemplary verification tasks which we carried out on State Machines and Composite Structures. In Chapter 14 we conclude with a summary and some suggestions for future work.

Part I

Background Material

Chapter 2

The Unified Modeling Language The Unified Modeling Language (UML) is a modelling methodology and a family of diagram languages which are widely used in software engineering. It was developed in the 1990s to unify the different object-oriented modelling methodologies in use, the number of which had increased to over 50 by 1994. The authors of three of these methods, Grady Booch, Ivar Jacobson and James Rumbaugh, at first adopted ideas from each other's methodologies and then began to actively cooperate in creating a common standard which unified the advantages of each. Their stated goals were as follows [START_REF] Booch | The Unified Modeling Language User Guide[END_REF]:

1. To model systems, from concept to executable artefact, using object-oriented techniques.

2. To address the issues of scale inherent in complex, mission-critical systems.

3. To create a modelling language usable by both humans and machines.

Since 1997, several versions of the UML have been standardised by the Object Management Group (OMG). The current version of the standard, UML 2.5.1 was released in 2017. UML is widely used in industry and taught in academia. [RHQH + 17] report that, although the use of UML in open-source projects has been regarded as relatively uncommon, they were able to extract a dataset of 93000 UML diagrams from over 24000 projects on GitHub. UML has a common mechanism -the Meta Object Facility (MOF) -to express the abstract grammars of the various model types, as well as the XML based standardised exchange language XMI and, with QVT (Query/View/Transformation), a family of model transformation languages.

Strictly speaking, the abstract grammar defines the notion of a UML model, parts of which can be rendered as diagrams or serialised in XMI. In the following, we will discuss diagrams and model elements without distinction, confident that the reader will remember that details of the graphical presentation are not part of the model as such.

The different UML sublanguages broadly fall into two categories: On the one hand there are static diagrams, which describe, e.g., data models (Class Diagrams) or the hierarchical composition structure of a system (Composite Structure Diagrams). On the other hand, there are dynamic diagrams, which capture run-time behaviour, e.g., State Machines and Interaction Diagrams. Static and dynamic diagrams can be related to one another, two common ways being to specify the behaviour of a component from a Composite Structure Diagram by means of a State Machine, and to specify types in a Class Diagram which are then referred to in a State Machine.

In this thesis, we present formalisations for the basic features of State Machines and Composite Structure Diagrams. UML has an extension mechanism by means of so-called profiles; we do not support this. Adding such support would be straightforward for profiles that only introduce syntactic restrictions. On the other hand, profiles can introduce so-called stereotypes and constraints, the semantics of which can be arbitrarily difficult to model.

In the following, we will introduce a simple security protocol and use it to illustrate our discussion of some UML diagram types.

Example: A Simple Security Protocol

In this section, we will introduce the example of a simple security protocol adapted from [START_REF] Il | Secure mobile RFID system against privacy and security problems[END_REF], which we will use for the remainder of this chapter to illustrate the different UML diagram types.

This protocol is meant to operate, e.g., at the entrance of a warehouse to allow only authorised goods to enter. Authorisation to enter is expressed by attaching an RFID chip, called a Tag, to the goods in question. The Tag may confirm that the goods have undergone a customs check, or have been checked to be free of explosives, or any other property we want to ensure for all goods in the warehouse.

Concretely, the protocol can be expressed as follows:

1.R → T : n R 2.T → R : ID ⊕ n T , h(n R , k) ⊕ n T
Participants of the protocol are a Reader (R) and a Tag (T). First, the Reader sends the Tag a nonce n R as a challenge. To this message, the Tag responds with a pair of values computed by cryptographic operations. The operations used are an exclusive or (written ⊕) and a hash function h, both of which can be realised on an RFID chip. The Tag holds two variables: ID and k. ID and the key k identify the system. n T is a second nonce, generated by the Tag. The Reader authenticates the Tag based on the following computation:

8 computed_n T = received from Tag (ID ⊕ n T ) ⊕ ID computed_h = (h(n R , k) ⊕ n T ) received from Tag ⊕ computed_n T if computed_h = h(n R , k) then authentication_success else authentication_ f ailure
In the above, the ID, the nonce n R and the key k are known to the Reader beforehand, but the nonce n T is not. The Reader sends its nonce R n , which need not remain secret, but must not be reused to prevent replay attacks. Based on its knowledge of the preshared secret k, the Tag can then construct its reply as indicated above. The Reader can then reconstruct first n T and from this the hash value constructed by the Tag, using ⊕'s self-inverseness. The computed hash is then compared to the expected one, leading to an authentication success or failure.

"Security protocols address the question of how one communicates 'securely' in an untrusted 'hostile' environment" [START_REF] Roggenbach | Formal verification of security protocols[END_REF]. By design, the above protocol includes communication between two entities: The Tag and the Reader. The enviroment is hostile in that anyone might obtain a Tag, approach the door from the outside and interpose a device under their control between the Reader and the Tag. Such an Intruder would be a third, undesired protocol participant. In the tradition of Dolev and Yao [START_REF] Dolev | On the security of public key protocols[END_REF], the Intruder will be able to read, modify or suppress any messages transmitted between the regular protocol participants.

The above protocol has the authentication property of aliveness, i.e., a protocol run can only be completed if the Tag has participated in some way. To be more precise, the Reader authenticates a Tag if a legitimate Tag was involved in some protocol run, although not necessarily the one with the Reader. A detailed discussion of these authentication properties can be found in [START_REF] Roggenbach | Formal verification of security protocols[END_REF].

In the following, we will give an introduction to the UML. Therein we will mostly focus on those UML sublanguages that we will also treat formally later on in this thesis. We take the ability of our chosen sublanguages to encode the protocol example as an indication of its ability to express real-world problems.

Class Diagrams

Class Diagrams consist of classes and related concepts (see Fig. 2.1 for an example). More precisely, they contain classifiers with their various kinds of relationships. A classifier classifies a set of values called its instances -it is, roughly speaking, UML's concept of a type, although there is also a particular kind of classifiers known as a datatype. The most common kinds of classifier are classes and interfaces, which behave mostly like the classes and interfaces which the reader will know from object-oriented programming.

Figure 2.1 shows some classes and interfaces which model participants in the simple cryptographic protocol from Sect. 2.1. The diagram shows interfaces and a class with inheritance relationships (the arrows) and associations (without arrows). Instances of Reader and Tag are meant to be the regular participants of the protocol. Intruder inherits from both, because it implements the protocols of both -the Intruder will act as a man in the middle. A classifier can have features. These include attributes and receptions for signals (as in the example) or for operations1. Attributes are just the familiar concept, except that what is an attribute in an implementation may also be expressed by an association in the model. The example shows an attribute seen of type List<Data>, which contains the data from all messages seen so far by the intruder. The difference between signals and operations is that the former are asynchronoussignals do not return, and execution continues without waiting for them to return -whereas the latter are synchronous -operations can be waited for and can also have a return value.

The example also shows associations between the DolevYaoIntruder class and the two interfaces. These associations specify by the numbers at the ends that we expect exactly one Tag and exactly one Reader to be associated with each DolevYaoIntruder. In general, associations can have more than two participants and can make additional requirements, e.g., in which directions the association should be navigable, that instances of one end should be considered aggregates or, as a special case, composites of instances of the other end, etc.

Attached on the right to the DolevYaoIntruder class is a comment. Comments can contain arbitrary text and can be attached to (in general: sets of) elements in arbitrary diagrams.

Finally, and importantly for us, a classifier can have an associated Behaviour, i.e., a dynamic diagram (e.g., a State Machine) specifying how it will react to signals and operation calls. However, formalising Class Diagrams themselves is outside the scope of our thesis project2.

State Machines

A State Machine is a dynamic diagram, modelling behaviour. That behaviour could, e.g., be associated with a class, specifying the behaviour of its objects. Let us consider as an example Fig. 2.2. At the most basic level, it is a graph: A set of vertices, representing control states, connected by edges, representing state transitions. In addition to the control states, transitions can depend on and modify a data state. For a State Machine associated with a class, the data state would consist of the attributes of an object of that class. We will refer to the combination of the control and data state as a configuration.

Transitions have labels of the general form trigger[guard]/action. Each of the three parts can be omitted. The trigger is an event which can cause the transition to be taken. Explicit triggers will usually be signal receptions or operation calls. The guard is a condition over the data state. Where the right event was received, the truth of the guard, given current data, decides which of the transitions can be taken. An omitted guard is always true. UML does not specify in what language the guards and actions are to be expressed. A mixture of natural language and computer languages is common in UML diagrams, particularly for early design stages, or where diagrams are made only for human consumption. Of course, in this generality, UML cannot be formalised. Our formalisation in Chapter 7 will include a fixed language for expressing guards and actions, which is suitable for tool-supported reasoning.

UML has a variant of State Machines used purely for specifying the input language of a classifier: Protocol State Machines are mostly like ordinary State Machines, but their states can have no hierarchy or other associated behaviour, and their actions are replaced by post-conditions.

In this thesis, we refrain from formalising choice states, hierarchy, state behaviour and Protocol State Machines, as well as the priority rules for completion events. We do not model (synchronous) operation calls, but only (asynchronous) signal receptions.

Composite Structure Diagrams

Composite Structure Diagrams describe so-called structured classifiers. A structured classifier is a classifier -again, by default that means a class -which is considered to have an internal structure. Some examples for our security protocol example can be seen in Fig. 2 between ports, possibly with a socket/circle pair in the middle). The diagrams can also show interfaces a port offers (the circles) or uses (the sockets).

In the example (Fig. 2.3), we first show systems with just one role; then the intended system, with the roles of Reader and Tag; and, finally, a system for a man-in-the middle attack, with the Reader and the Tag communicating through the Intruder.

Tools

In the following we will briefly describe some of the tool landscape available for UML.

Classical Modelling Tools

As of May 2022, Wikipedia3 lists no fewer than 49 UML tools, where the features considered relevant for comparison include support for UML2 and the languages for which code generation or reverse engineering exist.

Notably, these features do not include analysis methods of UML2 models, such as simulation, model checking, theorem proving or refinement.

Classical modelling tools provide support for UML models in the strict sense, i.e., following the abstract syntax as prescribed by the MOF-expressed UML metamodel. Apart from editing models, they can check constraints in the Object Constraint Language (OCL) and typically allow some form of model transformations and code generation in certain programming languages. This category includes Enterprise Architect4, according to [START_REF] Ozkaya | A survey on the practical use of UML for different software architecture viewpoints[END_REF] the most-used UML tool in industry, as well as the Eclipse Modeling Tools5.

Mostly in the academic realm, some formalisations and formal tools for UML sublanguages exist. More information on these can be found in Chapter 5.

PlantUML

PlantUML [pla] has been used to render all the UML diagrams in this thesis. Also, the formal languages we develop are meant to provide a bridge between the worlds of PlantUML and the verification framework HeTS by using a PlantUML-inspired syntax.

PlantUML itself is a tool mostly offering graphical rendering of UML diagrams, based on a simple human-readable textual language (see Fig. 2.4). There are integrations into various other tools, including Eclipse, Microsoft Word, Matlab and WordPress6. The author of a diagram can tweak many graphical features, but for the most part, the tool is meant to choose good defaults. For many diagram types, Graphviz is used as the underlying graph layout tool. In this chapter, we introduce the concepts of institutions (well-behaved logical formalisms with a notion of vocabulary) and theoroidal comorphisms (well-behaved translations between institutions). But, before we turn to a general discussion, let us first introduce a formalism which we can use as an example.

Chapter 3

Institutions and Comorphisms

Running Example: Modal Logics

Throughout this chapter, we will study a simple modal logic [START_REF] Lambert | Modal logic in computer science[END_REF][START_REF] Goranko | Modal logic[END_REF] in order to illustrate the concepts of institutions and comorphisms. Modal logic is concerned with the discussion of possible situations. To this end it includes an operator ⟨⟩ ϕ which indicates the possibility of a formula ϕ being true. Such logics can include different modality labels, each of which corresponds to a notion of possibility. For example, in a logic describing the weather, possibility of rain could mean that it rains somewhere or that it rains at some time. Thus, we would have a geographic and a temporal modality label.

For each notion of possibility we immediately gain a corresponding notion of necessity: Whatever cannot possibly be false is necessarily true. This gives us a pair of modalities for each label. In our weather example, geographic necessity of sunshine would mean that the sun shines everywhere, whereas temporal necessity of sunshine would mean that the sun always shines.

Modal logic is a widely applicable method of reasoning for many areas of computer science. These areas include artificial intelligence, database theory, distributed systems, program verification, and cryptography theory.

We will now use a multimodal logic as a running example for building up to the notion of institution.

Let M be a set whose elements we call modality labels and P a nonempty set whose elements we call propositions. Then, sentences are defined by the following grammar, where modality labels are referred to by m and propositions by p:

ϕ, ψ ::= p |¬ϕ |ϕ ∨ ψ | ⟨m⟩ ϕ
Necessity and the other propositional junctors can then be defined in the obvious way:

ϕ ∧ ψ := ¬(¬ϕ ∨ ¬ψ) ϕ ⇒ ψ := ψ ∨ ¬ϕ ϕ ⇔ ψ := (ϕ ⇒ ψ) ∧ (ψ ⇒ ϕ) [m] ϕ := ¬ ⟨m⟩ ¬ϕ
Fixing an arbitrary sentence ϕ, we can moreover define:

true := ϕ ∨ ¬ϕ false := ϕ ∧ ¬ϕ
In order to avoid ambiguity, we use the following operator precedence rules: Negation binds the most tightly; followed by, on one level, conjunction and disjunction; followed by implication; then equivalence; then the modal operators.

For our weather subject, we would use the modality labels M = {time, place} and the atomic propositions P = {sunny, raining}.

Then, we might wish time and place to relate in such a way that

(⟨place⟩ [time] sunny) ⇒ ([time] ⟨place⟩ sunny)
holds. In words this would be: If there is a place that is always sunny, there is always a sunny place. Of course, the converse would not be tautological. With some optimism for our food production we might claim:

⟨place⟩ ((⟨time⟩ sunny) ∧ (⟨time⟩ raining))

In words this would be: There are places where both sunshine and rain do occur. We will use this notion of modal logics to illustrate the definitions of institutions and theoroidal institution comorphisms. The logics we develop for UML sublanguages are related to the multimodal logics presented here, but somewhat more complicated through their inclusion of constructs from hybrid logic.

Why use Institutions?

What is a logic? To answer this question formally, Goguen and Burstall developed the concept of an institution [START_REF] Goguen | Introducing institutions[END_REF]. Their account contains all the standard ingredients: Signatures, sentences, structures and a notion of satisfaction. However, the collections of structures and, crucially, of signatures, are not simply given as sets, but as categories, i.e., each includes a notion of morphisms. Moreover, there are (several) notions of morphisms between different institutions.

Structure morphisms are, of course, well known in all areas of mathematics. The addition of signature morphisms and morphisms between institutions is particularly interesting for us in a software and systems specification context: By enabling us to reason about changes of notation, they simplify and justify code reuse, refinement and relationships between artefacts in different specification or programming languages. In our general research programme, they allow us to develop small semantics for parts of the UML and combine them by means of a general framework for heterogeneous specification. But already when we are specifying in one particular logic tailored to the problem at hand, we can apply established verification tools developed for different logics, even several different tools within one proof, as long as logics and their translations fulfil the requirements of Institution Theory.

Categories and Functors

We briefly recapitulate the notions of category and functor and introduce our notations for both. Definition 3.1 A category C is given by -a class Obj(C), with elements called objects, -classes C(X, Y), with elements called morphisms from X to Y, for all X, Y ∈ Obj(C), -an identity morphism 1 X : C(X, X) for each X ∈ Obj(X)

-composition1 operations _ • X,Y,Z _ : C(Y, Z) × C(X, Y) → C(X, Z) for all X, Y, Z ∈ Obj(C) satisfying 1 B • A,B,B f = f = f • A,A,B 1 A ( f • B,C,D g) • A,B,D h = f • A,C,D (g • A,B,C h) for all A, B, C ∈ Obj(C), f ∈ C(C, D), g ∈ C(B, C), h ∈ C(A, B).
F(O, O ′ ) : C(O, O ′ ) → D(F(O), F(O ′ )) for all O, O ′ ∈ Obj(C),
where we abbreviate F(O, O ′ )( f ) to F( f ), preserving identities and composition, i.e.:

F(1 O ) = 1 F(O) F( f • g) = F( f ) • F(g) Definition 3.3 A natural transformation ν between two functors F, G : C → D (written ν : F → G) is given by a morphism ν O : F(O) → G(O) for each object O ∈ Obj(C), satisfying the conditions that ν Y • F( f ) = G( f ) • ν X for all morphisms f ∈ C(X, Y).

Institutions

We are now ready to define institutions, which we will then illustrate by defining an institution for modal logics.

Mod I (σ)(M ′ ) |= I Σ ϕ ⇔ M ′ |= I Σ ′ Sen I (σ)(ϕ)
for all signatures Σ, Σ ′ and all Σ ′ models M ′ , Σ sentences ϕ and signature morphisms σ : Σ → Σ ′ .

The slogan for the satisfaction condition is: "Truth is invariant under change of notation" [START_REF] Goguen | Introducing institutions[END_REF].

We will freely abbreviate Sen I (σ)(ϕ) to σ(ϕ) and Mod I (σ)(M) to M|σ.

An institution as such does not include a notion of inference. There are established notions of an institution equipped with an inference system, see e.g. [START_REF] Mossakowski | Comorphism-based grothendieck logics[END_REF].

Example: An Institution for Modal Logics

We will now introduce an institution for the modal logics described in Sect. 3.1.

Definition 3.5 A modal signature Σ ∈ Obj(O) is a pair (P(Σ), M(Σ))
, where P and M are sets, giving us propositions and modality labels, respectively.

Example 3.6 In our weather example a signature Σ = (P, M) could be given as:

P = {sunny, raining} M = {time, place} Definition 3.7 A modal signature morphism σ : C(Σ, Σ ′ ) is given by -a proposition part P(σ) : P(Σ) → P(Σ ′ ) and -a modality part M(σ) : M(Σ) → M(Σ ′ ).
Given signatures Σ, Σ ′ , Σ ′′ and morphisms σ ∈ C(Σ ′ , Σ ′′ ), τ ∈ C(Σ, Σ ′ ), we define identities and composition:

P(1 Σ ) = 1 P(Σ) M(1 Σ ) = 1 M(Σ) P(σ • τ) = P(σ) • P(τ) M(σ • τ) = M(σ) • M(τ)
Example 3.8 Returning again to the weather example, we could have an embedding from a specialised Californian weather logic. There, sunshine, being almost universal, needs no mentioning. Rain, however, when it occurs, is the topic of every conversation. So the Californian weather signature Σ C would look as follows:

P C = {dripping} M C = {when, where}
This signature can then be embedded into our original weather signature Σ by the following morphism σ = (P(σ), M(σ)) : Σ C → Σ: Between two structures, there is a single morphism ≤! : M → M ′ if the world set, accessibility relations and proposition satisfaction in M are all subsets of their counterparts in M ′ . Otherwise, the set of morphisms is empty.

P(σ)(dripping) = raining M(σ)(when) = time M(σ)(
Example 3.11 Over our weather signature, worlds could be given as the Cartesian product of times and places, i.e. W(M) = W t × W p . Figure 3.1 shows a possible set of times with its accessibility relation; Fig. 3.2 shows the same for places. In these cases the relations would be extended to worlds by ignoring the other tuple component (places or times). The examples given are very simple in at least two ways that cannot be generalised to arbitrary multimodal logics:

1. Each world is accessible from each. To justify a more interesting relation, we could consider another modality nearby which holds in all nearby cities, defined as those reachable from our current location by a train journey. We could then indicate sunshine somewhere around here (⟨nearby⟩ sunny) or all around here ([nearby] sunny). Figure 3.3 gives an example relation for this modality. Likewise, in the case of time, modalities with more restrictive accessibility can be imagined, and are commonly used in temporal logics. In theories over our old weather signature, we might wish to use axioms ensuring this all-connectedness.

2. Time and place are effectively independent. If we wanted a relativistic weather logic, we would need to consider the space-time continuum. Worlds could not then be given by a Cartesian product of independent places and times. The two accessibility relations would then need to be stated directly over whole set of worlds, and time and space could interact. Such interactions between accessibility relations are common in practice. However, where the relations are independent, human and automated reasoning can often be simplified by exploiting this natural modularity.

The reader can easily imagine a proposition satisfaction relation for the worlds and the weather propositions given. Definition 3.12 We now define translation for multimodal sentences as the structural closure of proposition and modality translation:

σ(p) = P(σ)(p) σ(¬ϕ) = ¬σ(ϕ) σ(ϕ ∨ ψ) = σ(ϕ) ∨ σ(ψ) σ(⟨m⟩ ϕ) = ⟨M(σ)(m)⟩ σ(ϕ)
W(M ′ |σ) = W(M ′ ) R(M ′ |σ)(m)(v, w) ⇐⇒ R(M ′ )(M(σ)(m))(v, w) Sat(M ′ |σ)(w, p) ⇐⇒ Sat(M ′ )(w, P(σ)(p))
Example 3.15 Reducing general weather models to Californian weather models is slightly more involved than embedding sentences. A model given by

W(M ′ ) = {(Frisco, April 1)} R(M ′ )(time) = {((Frisco, April 1), (Frisco, April 1))} R(M ′ )(place) = {((Frisco, April 1), (Frisco, April 1))} Sat(M ′ ) = {((Frisco, April 1), raining), ((Frisco, April 1), sunny)} reduces to W(M ′ ) = {(Frisco, April 1)} R(M ′ )(when) = {((Frisco, April 1), (Frisco, April 1))} R(M ′ )(where) = {((Frisco, April 1), (Frisco, April 1))} Sat(M ′ ) = {((Frisco, April 1), dripping)}.
So we have dropped one proposition and "renamed" the accessibility relations as well as the remaining proposition. If the Californian logic additionally had no concept of time, we would drop one accessibility relation, but worlds would still carry time information, and the remaining accessibility relation would still only be renamed without being modified.

In any of these variations, consider a sentence the translation of which holds in all models of the translated signature. Then, by the satisfaction condition, the sentence must already hold in all those models over the original signature which arise as reducts of some model over the translated signature. In fact, all Californian weather models arise this way, so a sound proof system for general weather sentences would give rise to another sound proof system for Californian weather sentences. A general theory of such borrowings can be found in [START_REF] Cerioli | May I borrow your logic? (transporting logical structures along maps)[END_REF]. For our proof case studies, we establish a borrowing principle in Prop. 10.3.

Definition 3.16

The satisfaction relation for multimodal sentences and structures is defined by:

M |=ϕ ⇐⇒ for all w ∈ W(M), we have (M, w) |= ϕ (M, w) |=p ⇐⇒ Sat(M)(w, p) (M, w) |=¬ϕ ⇐⇒ (M, w) ̸ |= ϕ (M, w) |=ϕ ∨ ψ ⇐⇒ (M, w) |= ϕ or (M, w) |= ψ (M, w) |= ⟨m⟩ ϕ ⇐⇒ exists v ∈ W(M) s.t. R(M)(m)(w, v) and (M, v) |= ϕ
Then the following theorem establishes the satisfaction condition by a typical proof using structural induction over the grammar of sentences: Note that as before, sentences are translated forward and structures reduced backward. Signatures and their morphisms are translated forward.

(M ′ |σ, w) |= ϕ ∨ ψ case ⟨m⟩ ϕ: (M ′ , w) |= σ(⟨m⟩ ϕ) ⇐⇒ [def. form. trans.] (M ′ , w) |= ⟨M(σ)(m)⟩ σ(ϕ) ⇐⇒ [def. sat. rel.] (exists v ′ ∈ W(M ′ ) s.t. R(M ′ )(M(σ)(m))(w, v ′ ) and (M ′ , v ′ ) |= σ(ϕ))) ⇐⇒ [ from def. form. trans.: R(M ′ )(M(σ)(m))(w, v ′ ) ⇒ v ′ ∈ W(M ′ |σ) ] (exists v ∈ W(M ′ |σ) s.t. R(M ′ )(M(σ)(m))(w, v) and (M ′ , v) |= σ(ϕ)) ⇐⇒ [ IH ] (exists v ∈ W(M ′ |σ) s.t. R(M ′ )(M(σ)(m))(w,
We will actually use a slight variation of the notion of comorphism, which allows properties that are inherent in a signature of the source institution to be expressed by sentences in the target institution. To make this precise, we first extend signatures to theory presentations: Σ ϕ for all ϕ ∈ Φ} of the Σ-structures satisfying the sentences in Φ. A theory presentation morphism σ : (Σ, Φ) → (Σ ′ , Φ ′ ) is given by a signature morphism σ :

Σ → Σ ′ such that M ′ |= I Σ ′ Sen I (σ)(ϕ) for all ϕ ∈ Φ and M ′ ∈ Mod I (Σ ′ , Φ ′ ).
Theory presentations in I and their morphisms form the category Pres I .

Note that Φ can be an infinite set of sentences, making theory presentations more general than finitary notions of a specification. Definition 3.20 A theoroidal institution comorphism3 ν = (ν Sig , ν Mod , ν Sen ) : I → J is given by -a functor ν Pres : Sig I → Pres J inducing the functor ν Sig = Sig • ν Sig : Sig I → Sig J on signatures, -a natural transformation ν Mod : Mod J • (ν Sig ) op → Mod I on models and structures, and -a natural transformation ν Sen : Sen I → Sen J • ν Sig on sentences, such that for all Σ ∈ |Sig I |, M ′ ∈ |Mod J (ν Sig (Σ))|, and ϕ ∈ Sen I (Σ) the following satisfaction condition holds:

ν Mod Σ (M ′ ) |= I Σ ϕ ⇐⇒ M ′ |= J ν Sig (Σ) ν Sen (Σ)(ϕ) .
A theory presentation (Σ, Φ) over the institution I is translated via a theoroidal institution comorphism ν : I → J into the theory presentation ν Pres (Σ,

Φ) = (Σ ν , Φ ν ∪ ν Sen Σ (Φ)) over J where ν Sig (Σ) = (Σ ν , Φ ν ) and ν Sen Σ (Φ) = {ν Sen Σ (ϕ) | ϕ ∈ Φ}.

Example: A Theoroidal Comorphism for the Standard Translation

As an example of a theoroidal comorphism, we present the standard translation from our institution for multimodal logics into an institution for first-order logic. We will not present the latter institution in detail. The interested reader can find an example of a first-order institution in [START_REF] Diaconescu | Encoding Hybridized Institutions into First-order Logic[END_REF]. The standard translation is the established way of relating modal logics to predicate logic [START_REF] Blackburn | Hybrid languages[END_REF]. We will use an adapted version of it in our treatment of State Machines. Intuitively, it is best understood by observing that the sentence translation directly mirrors the semantics of multimodal logic.

Translation of signatures. Assume a multimodal signature Σ = (P, M).

We will here take a first-order signature Σ FOL = (S, F, Pr) to consist of three sets, giving us sorts (S), function symbols (F) and predicate symbols (Pr), respectively, which are compatible in the obvious ways. In our translation of modal logic signatures, we have just one sort, namely that of worlds, no function symbols, per proposition one predicate symbol Sat(p) for proposition satisfaction, and per modality label m one accessibility relation R(m). Observe how this mirrors the definition of multimodal models.

ν Sig (Σ) = ((S, F, Pr), Φ) S = {W} F = {} Pr = {Sat(p) : W | p ∈ P} ∪ {R(m) : W × W | m ∈ M} Φ = {}
If we wished to have axioms restricting the class of legal accessibility relations, as mentioned above, these could go into Φ. Here, however, we are going to allow all relations of appropriate type.

Translation of sentences.

For sentences, we first give a version of the translation indexed over a variable for the current world. This version we define by recursion over the argument sentence. Then, as needed for the comorphism, we define a version without the index by universally quantifying over worlds.

ν Sen w (p) = Sat(p)(w) ν Sen w (¬ϕ) = ¬ν Sen w (ϕ) ν Sen w (ϕ ∨ ψ) = ν Sen w (ϕ) ∨ ν Sen w (ψ) ν Sen w (⟨m⟩ ϕ) = ∃v : W.R(m)(w, v) ∧ ν Sen v (ϕ), where v is a variable not free in ϕ ν Sen (ϕ) = ∀w : W.ν Sen w (ϕ) Example 3.21 (⟨place⟩ [time] raining) ⇒ ([time] ⟨place⟩ raining) would translate to ∀w 1 : W.(∃w 2 : W.R(place)(w 1 , w 2 )∧ ¬∃w 3 : W.R(time)(w 2 , w 3 ) ∧ ¬(Sat(raining)(w 3 ))) ⇒ (¬∃w 2 : W.R(place)(w 1 , w 2 ) ∧ ¬ ∃w 3 : W.R(time)(w 2 , w 3 ) ∧ Sat(raining)(u)).
We can observe that the sentences of our specialised logic are more succinct than the corresponding first-order sentences. Note, however, that the latter can be somewhat shortened by adding a specialised translation for the necessity modalities.

Reduction of structures. First-order structures are functions that take each symbol to its interpretation: Sorts to nonempty sets, and function and predicate symbols to appropriate subsets of Cartesian products of interpreted sorts. We only have to handle structures that conform to the translation of the modal signature (P, M), which makes it straightforward to recover our multimodal structures:

ν Mod (M ′ ) = (M ′ (W), {M ′ (R(m)) | m ∈ M}, {M ′ (Sat(p)) | p ∈ P}) Chapter 4
The Algebraic Specification Language Casl and its Toolset HeTS This chapter introduces the reader to the technical setting for our proof examples and our implementation: first to the Common Algebraic Specification Language (Casl); then to the Heterogeneous Toolset (HeTS), a specification toolset based on Institution Theory in which Casl is the central language; then to Haskell, the language in which HeTS, including our extensions, are implemented; and finally to Parsec, the Haskell library used for all parsing needs in HeTS.

The Casl Language Family

In 1995, the Common Framework Initiative (CoFI) [START_REF] Peter | Cofi: The common framework initiative for algebraic specification and development[END_REF] was started to reduce the fragmentation of the field of algebraic specification. Convinced that there had been enough experimentation for the community to know which features, convictions and tastes should be considered in such an effort, CoFI set out to build a core language that should be acceptable to the whole community with comprehensive documentation and agreed principles for defining restrictions and extension of that language. In 1997 a language design was proposed, featuring abstract syntax and semantics, but deliberately leaving the concrete syntax open. Version 1.0 of the Common Algebraic Specification Language (Casl) was adopted in 2001. The current version (1.0.2) was adopted in 2003, with no further changes planned [START_REF] Bidoit | CASL User Manual: Introduction to Using the Common Algebraic Specification Language[END_REF].

The language Casl is the core output of CoFI. The comprehensive documentation, which the earlier, fragmented efforts were often missing, comes in the form of two manuals: The User Manual [START_REF] Bidoit | CASL User Manual: Introduction to Using the Common Algebraic Specification Language[END_REF] is an example-based introduction to the language and to some supporting tools.

It aims to be didactical rather than complete, but is still more comprehensive than we can be in this thesis. The Reference Manual, on the other hand, aims for completeness above all else. It provides a language overview, formal grammars for the abstract and concrete syntax of Casl, as well as the formal semantics [START_REF] Roggenbach | CASL reference manual[END_REF].

Several aspects of Casl can be understood and used largely independently from one another: Basic Specifications are a notation for many-sorted first-order theories with sort generation constraints, subsorting, partiality and equality. Much effort went into combining the availability of total and partial functions on the one hand with subsorting on the other hand. The language of Structured Specifications provides constructs for parameterising, modifying (by hiding and renaming of symbols) and combining Basic Specifications. The structuring here applies only to the presentation of the specification and does not affect the models. In contrast to this, Architectural Specifications can require structure and parameterisation of models (pragmatically speaking: of conforming software artefacts). Libraries are sequences of named specifications, where earlier specifications can be included by name in later Structured and Architectural Specifications.

Consider the specification of natural numbers in Fig. 4.1. Everything between Nat = and then is a Basic Specification. A Basic Specification introduces sorts, operation symbols and predicate symbols with type signatures, and axioms. In our natural numbers example, this is the order in which they are given, with one exception: With the free type construction we simultaneously introduce operation symbols for the constructors and axioms that requires the sort to be freely generated by the constructors. A sort could also be introduced with just generatedness or with no generation constraints at all. The meaning of these constraints is as usual, but can be summarised by the slogan "no junk, no confusion": essentially, for a generated type, all values can be written as constructor terms ("no junk"). This establishes an induction principle, which actually takes us somewhat beyond first-order logic. For free types, different constructor terms additionally have to stand for different values ("no confusion"). For the precise semantics, we refer the reader to the Reference Manual [START_REF] Roggenbach | CASL reference manual[END_REF]. Turning again to the example, we see three sections separated by then. This is the first structuring concept we will consider, that of extension. Each section here is spelled out directly, but we could also refer to other specifications by name. The later sections add symbols and axioms that can refer back to the earlier sections, e.g., a new operation can have a sort introduced in an earlier section. The reader will further notice that that axioms can be given names (here: decimal_def) and that then can be followed by annotations about the relationship of the following to the previous section. Here, the second section is a definitional extension of the first, and third merely adds implied axioms -when we come to proving, these will be our proof obligations.

Besides extension, Casl offers the structuring concepts of union, renaming and hiding of symbols, naming of specifications, and generic (parameterised) specifications, which will not here be discussed in detail.

Heterogeneous Tooling with HeTS

The Heterogeneous Toolset HeTS1 , 2 [MMCL14, MML07a] is a verification suite built around Casl and Institution Theory. It is written in the functional programming language Haskell [M + 10], and contains parsers for various formal languages, as well as translations between those languages. HeTS includes bindings to many existing verification tools. It provides proof support for heterogeneous specifications, i.e., specifications using more than one language. This heterogeneous verification is meaningful as long as the languages involved are institutions and the translations are theoroidal comorphisms, as introduced in Chapter 3.

We will now briefly discuss some screenshots and graphics to illustrate some principles of HeTS and our use of it, simultaneously giving the reader an impression of its user interface.

Figure 4.2 shows HeTS with a visualisation of its language graph. UMLState (leftmost in the top row) is a language we implement in this thesis for UML State Machines -more on this in Chapter 12. It is easy to see the central place of Casl as both the source and target of many translations. Our approach fits neatly into that picture: We use translations via Casl to borrow [START_REF] Cerioli | May I borrow your logic? (transporting logical structures along maps)[END_REF] existing verification tools for our new languages.

Specifications and verification tasks are represented as development graphs. An example of such a graph is shown in Fig. 4.3. A development graph represents a library, which is mostly like a Casl library, but allows the specifications contained in the library to be written in any of the logics implemented in HeTS, not just Casl itself. Here we see in action the independence of the Casl structuring concepts from the Basic Specifications. However, in addition to renaming, we Returning for a moment to the graph representation of libraries, we see that the nodes are Basic Specifications or specification extensions. The edges show that a specification is based on another, be it through translation from a different logic or through Casl structuring concepts. Some such edges, most importantly those corresponding to uses of then %implies (e.g., Fig. 4.1, line 39) give rise to proof obligations.

HeTS offers a graphical and a textual user interface for discharging such proof obligations.

The GUI interaction for a typical proof could go as follows: Figure 4.3 shows a development graph with named nodes for name specifications and unnamed nodes for intermediate extension steps (separated in HetCasl by the uses of then). Applying a rule from the heterogeneous proof system transforms this into the graph of Fig. 4.4. Here proof obligations have been turned into local proof obligations in a node (in red) in one logic. We will later deal with cases where proof obligations are localised into several nodes. Figure 4.5 shows the actions we can perform on the red node containing the proof obligation. Choosing the action Proof leads us to the window of Fig. 4.6, where we can configure our proof attempt. In particular, we can choose a prover, a comorphism into the input language of that prover, as well as a selection of axioms and proof goals to include. The interaction with the chosen prover then occurs through the window shown in Fig. 4.7. The selected prover here is Spass [WDF + 09], a fully automatic prover, so interaction is restricted to starting and stopping proof attempts with variations in timeout and other options.

A Short Introduction to Haskell

We will briefly introduce the reader to the three main aspects setting Haskell apart from most earlier functional programming languages, namely typeclasses, lazy evaluation and encapsulation of effects using monads. This section and the next were written as a Jupyter notebook3 with IHaskell4. This allows us to automatically display results of evaluation, type inference, etc.

Typeclasses

A typeclass can be thought of as a predicate with one or more types5 , 6 as arguments, together with certain values (the methods), the types of which can mention the typeclass arguments. The type expressions for the methods have to involve some of the argument types of the typeclass. The predicate is defined loosely: It is is always possible to add an instance for another combination of argument types.

This enables us to write programs with a constrained parametric polymorphism7: Expressions which are given solely in terms of the methods of certain type classes are available for all combinations of types implementing those type classes.

A simple example is the functor typeclass:

[1]: class Functor f where fmap ::

(a -> b) -> f a -> f b
fmap then has the constrained polymorphic type:

[2]: :type fmap fmap :: forall (f ::

* -> *) a b. Functor f => (a -> b) -> f a -> f b
Instances of this typeclass should be thought of as endofunctors, where objects are Haskell types, and morphisms are Haskell functions. Then the typeclass parameter f is the functor's object part and fmap is the morphism part. fmap promotes a function on so-called pure values to a function on functorial values. Of course, the same value can be thought of as pure or functorial in different contexts. It is common to require the instances of a typeclass to satisfy some laws -for functors, these are the usual preservation laws for identities and composition.

The following defines the Functor instance for the "list of' ' endofunctor:

Lazy Evaluation

Haskell uses non-strict evaluation. In practice, implementations use lazy evaluation, which is non-strict evaluation with sharing. Strictness can be explicitly enabled in certain situations.

Non-strictness here means that Haskell terms are only evaluated as far as is necessary. This usually means that when a function matches one of its arguments against a constructor8, the argument is evaluated until the constructor at its root is known. Failure to produce such a constructor, be it through non-termination or some other way, is represented by a special value ⊥, which each Haskell type contains.

For example, the following defines a nonterminating computation by a simple recursion:

[4]: regress = regress 7 Unconstrained parametric polymorphism is also possible.

The evaluation of regress would then fail to terminate. The follwing likewise produces ⊥, but through an incomplete case distinction: error, called at <interactive>:1:1 in interactive:Ghci117

However, non-strictness allows us to usefully define: In words, we can take the head of a list with undefined second element. We can likewise take a (sufficiently defined) infinite list and retrieve its seventh entry. Finally, we see that Haskell can compute the length of a list with an undefined element, since the length of a list only depends on its spine, formed by the constructors (:) (i.e., cons) and [] (i.e., empty list).

In this setting, a function argument has to be a representation of the computation that would produce both the constructor and the representation of the constructor's arguments. Haskell implementations avoid copying these representations, but instead pass them around by means of pointers, thus also avoiding the need to evaluate them repeatedly, which could arise in a naive implementation of non-strict semantics. For example, without this sharing aspect of lazy evluation, the argument to sharingFun would be copied and (partly) evaluated twice.

Sharing is an implementation detail, which does not show up in the denotational semantics and is not required by the Haskell standards. In practice, however, Haskell implementations use lazy evaluation, i.e., non-strict evaluation with sharing.

The theoretical underpinnings for strict and non-strict evaluation and their denotational semantics are to be found in domain theory [START_REF] Scott | Domains for denotational semantics[END_REF].

Monads: Encapsulating Side Effects

In Haskell, a function should be thought of as doing nothing beyond producing a value of its return type. This does not mean that effectful programs cannot be implemented in Haskell, only that their type must9 indicate which effects are possible.

A Monad is a special kind of Functor. Its type level function turns a type of values into a type of so-called monadic actions with result values of the original type. Monads must implement two methods, the first being:

return :: Monad m => a -> m a
This method takes a pure value and turns it into a computation that does nothing beyond returning that value. In other words, it allows us to consider a pure computation as an effectful one.

The second method of Monad is:

(>>=) :: Monad m => m a -> (a -> m b) -> m b
This method is pronounced "bind" and is, roughly, sequential composition of two actions. However, the second action can depend on the result of the first, so the actual second argument is a family of actions, as can be seen in the type signature.

These two methods are expected to satisfy:

1) the left identity law:

return x >>= f == f x
2) the right identity law:

9 There are ways around this, which we will not discuss here.

m >>= return == m

3) associativity:

(m >>= f) >>= g == m >>= (\x -> f x >>= g)
A Monad can be defined simply by implementing an instance of the Monad typeclass. Haskell has a special notation for writing monadic computations in an imperative style without losing the effect encapsulation:

[12]: import Control.Monad divisors :: (Integral a, Enum a, Show a) => a -> [String] divisors bound = do x <-[2..bound] y <-[2..x] guard (x 'mod' y == 0) return (show y ++ " divides " ++ show x) divisors 4 ["2 divides 2","3 divides 3","2 divides 4","4 divides 4"]
The above is a computation in the list monad, which can be considered to provide a non-determinism effect. Sequencing in the do-notation is equivalent to ordinary applications of (>>=), where the intermediate results are λ-bound.

In terms of list comprehensions, the above computation could be stated as:

[13]: divisors bound = [ show y ++ " divides " ++ show x | x <-[2..bound] , y <-[2..x] , x 'mod' y == 0 ] divisors 4
["2 divides 2","3 divides 3","2 divides 4","4 divides 4"]

Haskell provides an IO-Monad, which contains most effects one would usually expect from an imperative programming language, including File IO, mutable variables and concurrency. Beyond this, there are many specialised Monads, to which, as mentioned, the user can easily add. One of the areas where such monads have proved very successful is parsing, to which we will turn our attention in the next section.

Parsec

The parsers of the various input languages of HeTS are implemented using Parsec [START_REF] Leijen | Parsec: A practical parser library[END_REF]. Parsec is a library of monadic parser combinators for Haskell and, to our knowledge, was the first industrial strength parser combinator library. As of 13th of June 2022, 1023 packages on Hackage10 depend on parsec11 and a further 907 on the attoparsec12 library built on similar principles.

Parser combinators, in contrast to parser generators like yacc, are directly implemented as functions in the host language.

We will show the use of Parsec by means of the classic expr language from [START_REF] Aho | Compilers: Principles, Techniques, and Tools[END_REF]. To do so, we first recapitulate its grammar in the form of Haskell type declarations. The grammar defines the problem which the parser then solves.

The particular language we are dealing with consists of simple arithmetical expressions without variables, with the usual operator precedence rules. The above are (the parse tree types of) the nonterminals of the expr language. The constructors (:+), (:-), (:*) and (:/) encode the basic arithmetic operators. Next, we will bring relevant modules into scope and define the type for our parsers: In Parsec, a parser can parse some type of streams (here: String), keeping state of some type (here: (), so we are not keeping any state) and give a result of some type (the type variable t, as we have several different parse tree types). Now, it is time to see the first parser:

[16]: digitP :: Parser DIGIT digitP = oneOf ['0'..'9'] <?> "DIGIT"
Here we used two parser combinators: oneOf and (<?>)

Given any list cs of characters, oneOf cs consumes the first character c and, if c `elemc s, returns it. If the character does not match, an error occurs: [17]: parseTest (oneOf ['0'..'9']) "5a" '5'

[18]: parseTest (oneOf ['0'..'9']) "a5" parse error at (line 1, column 1): unexpected "a"

The combinator (<?>) takes a parser p and a string s, describing the unit we want to parse. The parser p <?> s behaves just like p in the case of success, but uses s to give more meaningful error messages in the case of parse failures:

[19]: parseTest digitP "a5" parse error at (line 1, column 1): unexpected "a" expecting DIGIT Parsers can have values of any type as their result, including functions. We will make use of this in the following auxiliary definitions:

:: a -> (a->b->c, b) -> c op a (f,b) = f a b
Here, we combine alternative parsers with (<|>). Parsec tries to parse the first option. If that fails without consuming any input, the second one is tried. If, however, the first parser does consume input, we are committed to that option. This behaviour is due to the ineffeciencies that would arise if Parsec always preserved the information required for backtracking. However, controlled backtracking can be introduced throught the try combinator: Where p would fail after consuming input, try p will fail without consuming any.

We have seen two more new combinators: char has the obvious meaning. The ($>) combinator combines a parser p with a pure value v. The resulting parser returns v if p succeeds.

The remaining parsers refer to each other, so we present them together: New combinators used here are:

-(<$>): This is the same as fmap and is available for all functors. In the case of parsers, f <$> p parses with p and applies f to the result.

many: Parses zero or more matches of its argument parser, collecting the results in a list.

-(*>) and (<*): Each of these combines two parsers, ignoring the result of the first ((*>)) or the second ((<*)).

This should be sufficient to aquaint the reader with the ideas underlying Parsec and to handle many common parsing problems. The complete API reference of Parsec is available at https://hackage.haskell.org/package/parsec. We now turn to a comparison of our work with other approaches to the formalisation of and verification of properties for parts of the UML. The approaches we found fall into the categories of fully automatic model-checking on the one hand, and the use of interactive theorem provers on the other hand. In contrast to the model-checkers, the provers can be applied where infinitely many states have to be considered. However, this is bought with a partial loss of automation.

For each approach, after a general description and a comparison with our approach, we summarise one or more examples which the authors of the approach have used to illustrate the same. These example summaries are not meant to make separate points about how each approach compares to ours, but rather to support the reader's imagination in reflecting the goals, methods and potential of each approach.

A number of other authors give formal semantics to communicating State Machines, however with a purpose different from symbolic analysis of UML. Most authoritatively, the Object Management Group provides an executable semantics of UML Composite Structures [START_REF]Precise Semantics of UML Composite Structures[END_REF]. Their objective is to provide an interpreter for the executable subset fUML of the UML. However the approaches we discuss in more detail here are all focused on symbolic analysis.

Closely related to our approach are the works [START_REF] Knapp | An Institution for Simple UML State Machines[END_REF][START_REF] Knapp | UML Interactions Meet State Machines -An Institutional Approach[END_REF]. Both these papers address the topic of communicating state machines, however, both fail to provide entirely correct institutions of State Machines. Learning from the reason for this shortcoming, rather than capturing UML state machines directly as an institution, in Chapter 7 we build up a new logic in which UML State Machines can be embedded. In Chapter 9, we extend this logic for communication. In particular, we treat UML event pools as part of Composite Structure Diagrams rather than of State Machines. State Machines are seen as a completely open system, which is (partially) closed by 'wiring up' in a communication structure. Overall, this leads to a separation of concerns: event pools and transitions can be analysed independently. Chapter 7 contains additional details on how our work is related to theirs, so we will not dwell on this here. Next, we will discuss several approaches that fall into the two categories we outlined in a bit more detail.

Automatic Verification of Finite UML Models

First, let us consider two examples of the fully automatic approaches, one using SAT-solving, the other using the UMC model-checker.

"Verifying UML/OCL Models Using Boolean Satisfiability"

Soeken et al. [SWK + 10] use SAT solving to tackle a class of UML verification problems. Given a Class Diagram, a set of OCL constraints, and finite bounds on the number of objects and on the domains of attributes, they generate propositional formulae. SAT solving on these formulae can then determine whether a satisfying instantiation exists and whether the OCL constraints are free of redundancy. The authors report having implemented this approach in a C++ tool. They have performed benchmarks, in which they report obtaining better verification times than the existing tools USE and Alloy in those cases where a comparison was possible.

We see the main advantage of this approach in the highly tuned tools which are available for SAT solving. In terms of structure, their treatment is more general than ours, in that we only treat the fixed structures described in Composite Structure diagrams, whereas they treat Class Diagrams, in which associations can admit a range of cardinalities, and the number of total instances is not fixed. However, their approach is only concerned with structure, whereas our focus is on behaviour. Moreover, the theory of institutions allows our approach to be integrated with other parts of UML and other specification mechanisms.

As an example, Soeken et al., discuss a verification problem over the Class Diagram in Fig. 5.1. The diagram specifies a processor in relationship to its registers, for both of which classes are given. Further, the diagram contains an enumeration type used for encoding the purpose of a register. Multiplicities require each register to be linked to exactly one processor and each processor to one or more registers. Attributes specify, among other things, a bitwidth for each register and for each processor. An OCL constraint requires the bitwidths of a processor's registers to equal that of the processor itself.

Figure 5.2 shows a finite system state over this Class Diagram. It further shows how that system is encoded into propositional variables, i.e., variables ranging over bits: Each link (represented by a ⃗ λ value) between objects and each attribute (represented by an ⃗ α value) is represented by, in this case, one, three, or eight bits. For the links, each bit encodes the presence or absence of that link to one of the appropriately typed objects. For the attributes, strings are here abstracted to a 2 bit representation, a register's purpose uses three bits for the four cases of the enum and the special value null. The integers representing bitwidth are here restricted to eight bits each.

Soeken et al. can then express properties over system state by propositional logic formulae.

For example, they express the OCL constraint from Fig. 5.1 as . This replaces the forAll over a known finite number of registers by the conjunction of a finite family of propositional formulae. Each register is only considered if it is linked to the one processor. Then, the bitwidth attributes are required to agree -the equation is shorthand for the obvious propositional equivalences between corresponding bits. In like manner, the Class Diagram itself is encoded into propositional formulae.

SAT solving over these then yields information about the specification's consistency: If the SAT solver returns a satisfying assignment of the propositional variables, this corresponds to a valid system state, and the specification is consistent. If the formulae are reported to be unsatisfiable, there is no valid system state conforming to the bounds imposed, but the Class Diagram and OCL constraints may or may not be consistent. If SAT solving does not complete within acceptable resource bounds, no information is gained, of course.

Verification tasks other than consistency can likewise be checked using a SAT solver. This requires encoding the verification task as another propositional formula, included in the SAT problem given to the solver -the verification flow is shown in Fig. 5.3. The authors report verifying the independence of certain OCL constraints from certain models, where a constraint is considered independent if it is not implied by the requirements of the model itself.

"From EU Projects to a Family of Model Checkers"

UMC1 by terBeek et al. [START_REF] Beek | From EU projects to a family of model checkers[END_REF] is a modelling language and associated model checker meant to correspond to a subset of UML. It is part of the KandISTI suite for on-the-fly model-checking. UMC provides a language for specifying classes, each with an associated State Machine, a statically determined set of objects instantiating those classes and a set of abstraction rules. The State Machines can be hierarchical. The abstraction rules determine which aspects of the system should be visible during model-checking. Each system so specified is closed off from the outside world in that no messages can enter or leave it. UMC then provides a fully automatic tool to check its temporal logic UCTL against such models.

UMC supports more features of UML State Machines than do we. However, for the features we do support, our approach has mainly one advantage in principle and one in terms of tools: It is somewhat more general in principle in that we show properties that a State Machine -or a system of such -has in all possible contexts, whereas UMC checks properties in one particular context. This one context can of course contain a nondeterministic machine modelling an almost arbitrary environment. However, the nondeterminism only applies to control states, and therefore, to finitary branching. Branching between arbitrary values from an infinite data type is not possible in an approach based on state enumeration. In terms of tools, our approach makes several, ideally all formal methods tools available to establish a property -this could include UMC in those cases to which it is well suited. One case-study to which UMC has been applied is the prevention of deadlocks in railway routing. We will base the remainder of this section on a paper reporting on this case study, namely [MSLF14] by Mazzanti et al, wherein they provide a tool-supported process (Fig. 5.4) for modelling an Automatic Train Supervision system (ATS). The ATS routes metro trains between stations, ensuring that each of the trains will eventually arrive at its final destination. This implies that the ATS has to prevent deadlock situations. Deadlocks arise when trains block each other, which translates straightforwardly into a classical resource-based formulation of deadlocks: Trains that move acquire and release track segments, where the segments are considered not at the signalling level, but somewhat more abstractly. A deadlock then exists iff all movements of trains from their current position would require the previous release of some track segment.

The approach starts with a discrete-time model given by a collection of trains. Each train has as its state a current point and a mission, i.e., a list of points it ought to traverse. The missions of all trains form the overall metro network layout. An example layout can be seen in Fig. 5.5. At this modelling stage, the system can make a transition iff there is a train whose next mission point is unoccupied. The further modelling process then essentially consists in finding further conditions that prevent deadlocks from arising.

To enable the formulation of such conditions, the authors give criteria for identifying basic and then composite critical sections. For each such section, they extend the system state with a counter for the trains present in that section and another variable indicating its capacity. Deadlocks in basic sections arise by trains moving in opposite directions or by a cyclic section's being completely filled with trains, none of which can leave the cycle.

The model is updated with conditions preventing these deadlocks and with actions updating the counters. Figure 5.6 shows an example of a possible resulting transition rule. Then, model-checking is used to detect two conditions which necessitate another iteration:

1. There are still deadlocks, so some more composite critical sections must be identified. This situation is identified by defining the abstraction rule in Mazzanti et al. [START_REF] Mazzanti | Deadlock avoidance in train scheduling: a model checking approach[END_REF] further discuss how to make the sizes of state spaces more manageable by checking different regions of a layout separately. SA to SF are train counters for critical sections. The two-dimensional array G1C (an example defined in Fig. 5.8 prescribes how movements of Green1 affect these counters. Each critical section counter also has a prescribed maximum value.

Figure 5.7: An abstraction rule from [START_REF] Mazzanti | Deadlock avoidance in train scheduling: a model checking approach[END_REF] for detecting deadlocks. For a system with two green trains and two red ones, the abstract name ARRIVED is given to system states where each train's position is the final one in its mission (here 13 for all).

Interactive Verification of Potentially Infinite Models

Having seen two examples of fully automatic UML verification approaches, we now give three examples of interactive approaches: First we discuss an approach using the PVS prover; then a second one, which builds a notion of system models within the Isabelle theorem prover; and finally, an approach based on symbolic execution and on the KIV prover. The approach is similar to ours in many ways. Verification is done by first translating into a conventional logic of an existing prover. Again, their treatment includes Class Diagrams and OCL constraints and is therefore more general than ours in terms of structure. In terms of behaviour it covers a similar subset of UML State Machine features. At the intersection of structure and behaviour their approach, unlike ours, covers object creation. Being a symbolic approach like ours, it can deal with properties that involve infinitely many configurations. Like us, they encountered the difficulties of reasoning about message queues.

"Formalising UML Models and OCL Constraints in PVS"

Our approach goes beyond theirs in the following ways: We give principles of inductive proof steps with invariants that could be automatically generated (see Chapter 13). This will, of course, never cover all proofs and lemmas for all verification tasks. Where it is possible for our translations, it will usually also be possible for theirs if one makes use of the advances in proof automation and computation power that have been made since 2005. A further advantage of our approach is, again, the multiplicity of tools we have available for proving. But already in terms of specification itself we profit from the modularity provided by Institution Theory. The authors of [KFdB + 05] in giving a joint formalisation for Class Diagrams, State Machines and OCL, cannot just compose existing formalisations of the subformalisms. Extending their approach to a larger fragment of the UML suffers from similar problems. Our approach, on the other hand, can more easily integrate formalisations of other subformalisms of UML, as well as unrelated formalisms, as long as the formalisms are institutions and suitable comorphisms are given. Kyas et al. show the application of their approach to the example of the Sieve of Eratosthenes, a classical technique for generating prime numbers. They verify the property that the generated numbers are actually primes.

Figure 5.9 shows their architecture, consisting of the classes Generator and Sieve. There are associations from Generator to Sieve and from Sieve to Sieve, which are both called itsSieve.

The system contains exactly one Generator, the behaviour of which follows Fig. 5.10. It starts by creating the first Sieve. The generator keeps a counter x, which must at first be initialised to 2. Every 20 time units, the value of x is forwarded to the first Sieve, after which x is incremented.

Each Sieve behaves in accordance with Fig. 5.11. A Sieve repeatedly receives numbers. The first number so received must be prime and is stored in the attribute p. After that, a successor Sieve is created, and each further number that is received is tested for divisibility by p. If it is divisible, it is silently dropped, otherwise it is forwarded to the next Sieve. In this manner, a pipeline of Sieves is constructed, corresponding to a linked list of all primes less than x. If x is passed through to the last Sieve in the pipeline, it is not divisible by any smaller prime and, therefore, is prime itself. The authors express this safety property by the following OCL constraint:

In words: In any Sieve, p only takes values divisible by no number from 2 to p -1.

The authors have developed a compiler that generates the specification corresponding to the diagrams in PVS, and likewise the verification goal. Figure 5.12 shows the result of translating a transition from Fig. 5.11 into PVS. In particular, it shows definitions for -a TYPE+ (i.e., a non-empty type), giving the locations (i.e., control states) for both State

Machines by an enumeration of nullary constructors;

-the Transition itself, given as a record of a source, a trigger, a guard, a list of actions, a target, and the class to which the transition belongs, whereof the guard is of function type, making use of PVS's higher-order capabilities; and -a setof[Transition], stating which transitions are available in the whole system of a Generator and Sieves.

The goal turns out to depend on particular properties of the event queues. After formulating and proving these as lemmas, the authors were able to prove the safety property.

"System-model Based Definition of Object-Based Modelling Languages with Semantic Variation Points" (title translated by us)

Grönniger [START_REF] Grönniger | Systemmodell-basierte Definition objektbasierter Modellierungssprachen mit semantischen Variationspunkten[END_REF] defines a notion of model for object based systems (called a system model).

A model (in the sense of UML) in a UML sublanguage is then interpreted to select a set of conforming system models. The author further proposes a general approach to treating variation points in the concrete and abstract syntax, as well as the semantics of modelling languages. Grönninger applies this approach to variation points of the UML. He provides a translation of several UML sublanguages to Isabelle/HOL, and a formalisation of the theory of system models in the same language, thus providing a proof tool. Compared to our approach, the main theoretical difference of the system model approach is its complexity, due to the need to treat all aspects of all possible object based systems. Their treatment is modular in the sense that it is given by structured theories, but if at any point a variation on the notion of system model itself became necessary, this would lead to new, not easily comparable, model classes for existing UML models. Properties once thought established would be subject to doubt again. Likewise, translations into a complex formalism involve many possibilities of making bad choices, which likewise would be hard to undo without losing established results.

In terms of tools, the system model is formalised in Isabelle/HOL. The interactive Isabelle system contains integrations of several automatic provers. Isabelle/HOL is also integrated into HeTS, allowing to some extent the highly principled tool reuse and formalism combination that Institution Theory permits, although with some difficulties: Reuse of existing tools for the system model formalism would require comorphisms out of higher-order logic. For these comorphisms to exist, the target logic would need to have signatures and sentences corresponding to all signatures and sentences of higher-order logic. Going in the other direction, translations from another formalism into Isabelle/HOL would not usually result in sentences over the system model signatures, requiring significant formalisation effort within Isabelle to establish a relationship. The somewhat arbitrary nature of this formalised relationship would then impair the usefulness of the guarantees Institution Theory gives us.

That said, the system model approach gives a useful semantics to a significant subset of UML, which makes a powerful tool available to the modeller and provides an integrated view of what an object based system can be. That view, even if we should find it too complex to connect to formally, can still inspire our approach to modelling parts of such a system and the relationships between such models.

We will now discuss three example systems verified by [Grö10] using the system model approach.

The first such verification task refers to the Class Diagrams shown in Fig. 5.13. The inheritance relationships specified in the two diagrams constitute a cycle. The author then shows, for a particular language variant, that this cycle makes the combination of these two diagrams inconsistent. As discussed, Grönninger [START_REF] Grönniger | Systemmodell-basierte Definition objektbasierter Modellierungssprachen mit semantischen Variationspunkten[END_REF] studies language variation points. Choices with respect to such variation points can be combined in a language configuration file, which can however leave some options unspecified. An example of such a file is given in Fig. 5.14. This configuration selects, among others, the variant AntiSymSub, which requires the subclass relation to be antisymmetric. The verification task at hand can only be carried out if this variant is active.

The configuration and the diagrams are translated to Isabelle. The diagram languages are deeply embedded into Isabelle, so the diagrams are translated into an explicit representation of their syntax. Based on the configuration, there is an axiomatisation for a semantic function, which is likewise represented explicitly in Isabelle as a thing to be reasoned about. The lemmas shown in Fig. 5.15 then establish that, in a valid system model, subclass relationships cannot be cyclical and must be transitive. The theorem shown in Fig. 5.16 then concludes that the two diagrams from Fig. 5.13 are in fact incompatible, i.e., that the sets of system models satisfying each have an empty intersection. As a second example, the author discusses the modelling of a calendar. First, the general concept of a calendar is modelled in a Class Diagram (Fig. 5.17). The Class Diagram models points in time via the DateTime class and then, using these, models calendar entries (class: Entry), where a calendar entry is given by a start time and an end time. Further, an Object Diagram is given (Fig. 5.18). The author then shows a lemma (Fig. 5.19) which restates the invariant from the Class Diagram and proves that this holds in all reachable states of system models conforming to the Class Diagram. Another lemma (Fig. 5.20) is shown, which restates As a third example, an authentication system is discussed, which is specified by the State Diagram in Fig. 5.22. The Sequence Diagram Fig. 5.23 then shows a run where the system authenticates a user who offered an incorrect key. After several lemmas, which we do not show here, the author proves the theorem Fig. 5.24, which shows that the State Chart rules out the run from the Sequence Diagram.

"Interactive Verification of UML State Machines"

Balser et al. [BBK + 04] provide a calculus for temporal logic into which they embed UML State Machines. They implement their calculus in the interactive theorem prover KIV. The tool Hugo/RT provides a translation of XMI files into the temporal logic, thus connecting their approach to any full-featured UML modelling tool on the input side. They then use KIV to verify properties stated in the same temporal logic.

Our approach is a direct successor of theirs. It results from the ongoing effort to find formalisations and translations of State Machines that satisfy the coherence conditions of Institution Theory. We found a difficulty in principle of such approaches in our Master's thesis [START_REF] Rosenberger | Relating UML state machines and interactions in an institutional framework[END_REF] and developed a modal logic of State Machines up to refinement, with an embedding of fully refined State Machines into that logic. The logic we formalise and implement in this thesis for State Machines is a development on the logic from our Master's thesis. More on the underlying problems and our approach to solving them can be found in Chapter 7.

A main advantage from [BBK + 04] for the user of their proof tool is their use of symbolic execution. In future work, we may well want to integrate a similar feature into HeTS, either for generating lemmas supporting fully automatic verification, or for discharging certain proof obligations by that mechanism itself.

We also make use of KIV to verify an example of a Composite Structure, however, we only use KIV's first-order and inductive capabilities, and only in a fully automated fashion.

In terms of examples, Balser et al. prove a property about an ATM scenario, an example family that is often found in the literature. We ourselves have performed proofs on a similar example, which we will discuss in Sect. 13.2. Their form of the example contains one class, Bank, for which a Class Diagram and State Machine are shown in Fig. 5.253. Over this system, they want to prove that, in all reachable configurations with control state DispenseMoney, it holds that the maximum number of tries has not been exceeded and the flag PINValid has been set. They express this through the formula:

Figure 5.26 shows the flow of information by which the authors transform such a State Machine into a form usable for proving: First, a suitable UML editor is used to create the diagrams. The editor must be able to export the diagrams in the XMI format. The tool Hugo/RT, developed by the authors of the paper, can then be used to translate from XMI into a KIV specification, from which desired properties can then be proved.

For the example at hand, after fixing an initial condition and an invariant, Balser et al. arrive at the proof graph shown in Fig. 5.27. It is worth stressing that the proof graph is not a tree because states that can be reached by several paths are nevertheless treated only once -the authors refer to this as sequencing. The structure of the proof graph is closely linked to the possible runs of the State Machine. Each proof step is either directly the execution of a State Chart step, or it expresses sequencing, or the application of the inductive hypothesis. The numbers on the nodes of the proof tree refer back to the states shown in Fig. 5.25 -a close inspection of this correspondence will do much to support the reader's intuition for how the symbolic execution supports the proof development.

Part II

Methodology Construction

Chapter 6

A Bird's-eye View of our Languages

In this chapter, we give an overview over the input languages, logics and translations developed or used within this thesis project and our two-stage process for developing them.

The most important points in this respect are summarised in Fig. 6.1: Arranged vertically, we have several formal logics, which are established or conjectured to be institutions, with (theoroidal) comorphisms translating between them. This starts at the top with our institution for UML Composite Structures. Then, we have our modal logic for event/data systems in two variants: EDHML (Event/Data Hybrid Modal Logic, without output events) and EDHMLO (with output events). Composite Structures translate into the latter variant. From our modal logics, we can then translate into CASL, the central logic of the HeTS framework, in which we are working. From there, we have translations to the tool-facing logics. Of these, we have used SoftFOL via an automatic and KIV via a manual translation. Other tool-facing languages could be added here. SoftFOL and the fragment of KIV we use (first-order logic with inductive data types) are standard enough that a violation of the Satisfaction Conditions for institutions or comorphisms seems unlikely here. To our knowledge, however, these results have never been formally established, so they remain conjectural.

Our input languages somewhat depart from the institutional logics. In the Composite Structures institution, which is built over EDHMLO, we have merely factored out the underlying State Machines. In the case of the State Machines, there is a larger difference: There are technical difficulties to directly creating a language for State Machines that is an institution1. Therefore, we needed to create a more expressive modal logic, which is a bit further removed from the structure of machines themselves. Sentences in this logic demand the presence or absence of certain transitions and could be regarded as expressing machines up to refinement. There is then an algorithm for constructing a formula that requires exactly the behaviour of one particular State Machine. This algorithm corresponds to the semantic function in Fig. 6.1, from outside the institutional world (depicted as coming from the side rather than above), and embeds State Machines (with or without outputs) into the relevant modal logic institution.

As mentioned before, we developed our languages in two steps. The first step treats State Machines in isolation, i.e., they can consume inputs, but their actions include no communication. Actions here are limited to updating the data of the local configuration. For these machines, we have developed the input language UMLState and the institution EDHML. In our EDHML the relevant notion of possibility is that of a machine allowing a particular kind of transition. The modality is a specification of the events consumed in such a transition. The formula under the modality makes requirements of the state in which we arrive, which can themselves again be modal formulae describing further transitions. The reader will observe that our logic does not necessarily fix the exact set of transitions possible in a machine, but gives a loose specification that can allow further refinement. This is by design and is the key ingredient to formula and structure translations that fulfil the Satisfaction Condition. We then describe an algorithm for translating a particular State Machine into that logic.

UMLStateO

The contents of this chapter have appeared in similar form as part of our paper at WADT 2020 [START_REF] Rosenberger | Institution-based Encoding and Verification of Simple UML State Machines in CASL/SPASS[END_REF].

The construction of EDHML was a common effort between Alexander Knapp, Markus Roggenbach and myself. In our virtual meetings, we jointly sketched the constructions, proofs and examples, which I then worked out in detail and wrote down in their final form. . The red transitions are those one would usually show in a UML State Machine. In UML, by default, an event is implicitly discarded if it occurs in a state where it is not explicitly handled.

Here, these dicarding transitions are displayed in grey. -consume reset, returning to s1, now with cnt = 0; and, finally -consume another reset, again leaving us at an unchanged s1 with cnt = 0 via the rightmost grey self-loop on s1.

Example: The Counter Machine

Event/Data Structures and the Problem with Institutionalising UML State Machines

It is for such simple UML State Machines as the counter in Fig. 7.1 that we want to provide proof support in Spass, one of the provers integrated into HeTS, via an institutional encoding in Casl. The sub-language covers the following fundamental State Machine features: data, states, and (non-deterministic) guarded transitions for reacting to events. However, for the time being, we defer all advanced modelling constructs, like hierarchical states or compound transitions to future work. An extension of UMLState with communication between machines will be presented in the following chapters in the form of the languages UMLStateO (State Machines with outputs) and UMLComp (Composite Structures).

In the following we first make precise the syntax of the machines by means of event/data signatures, data states and transitions, guards and effects. Then we introduce semantic structures for the machines and define their model class. Syntax and semantics of simple UML State Machines form the basis for their institutionalisation. We thus also introduce event/data signature morphisms and the corresponding sentence translation and structure reducts in order to be able to change the interface of simple UML State Machines.

Event/Data Signatures, Data States and Transitions

We capture the events for a machine in an event signature E that consists of a finite set |E| with elements called events and a map υ(E) assigning to each e ∈ |E| a finite set with elements called variables, where we write e(X) for e ∈ |E| and υ(E)(e) = X, and also e(X) ∈ E in this case. For the data state, we use a data signature A consisting of a finite set with elements called attributes. An event/data signature Σ consists of an event signature E(Σ) and a data signature A(Σ).

Example 7.1 The event/data signature Σ of the simple UML State Machine in Fig. 7.1 is given by the set of events |E(Σ)| = {inc, reset} with argument variables υ(E(Σ))(inc) = {k} and υ(E(Σ))(reset) = ∅ such that inc(k) ∈ E(Σ) and reset ∈ E(Σ); as well as the data signature A(Σ) = {cnt}.

For specifying transition guards and effects, we exchange UML's notorious and intricate expression and action languages both syntactically and semantically by a straightforward Casl fragment rendering guards as data state predicates and effects as data transition predicates, which, in the implemented language, take the form of assignments.

We assume given a fixed universe D with elements called data values and a Casl specification Dt with a dedicated sort dt in its signature Sig(Dt) such that the universe dt M of every model M ∈ Mod Casl (Dt) is isomorphic to D, i.e., there is a bijection ι M,dt : dt M ∼ = D. This puts at our disposal the open formulae F Casl Sig(Dt),X over sorted variables X = (X s ) s∈S and their satisfaction relation M, β |= Casl Sig(Dt),X φ for models M ∈ Mod Casl (Dt), variable valuations β : X → M, and formulae φ ∈ F Casl Sig(Dt),X .

Example 7.2 Consider the natural numbers N as data values D. The Casl specification in Fig. 4.1 characterises N up to isomorphism as the carrier set of the dedicated sort dt = Nat. It specifies an abstract data type with sort Nat, operations +, 0, suc, and a predicate < .

The very simple choice of D capturing data with only a single sort can, in principle, be replaced by any institutional data modelling language that, for our purposes of a theoroidal institution comorphism (see Chapter 8), is faithfully representable in Casl; one such possibility are UML class diagrams, see [START_REF] James | Designing Domain Specific Languages -A Craftsman's Approach for the Railway Domain Using CASL[END_REF].

Data states and guards.

A data state ω for a data signature A is given by a function ω : A → D; in particular, Ω(A) = D A is the set of A-data states. The guards of a machine are state predicates in F D A,X = F Casl Sig(Dt),A∪X , taking A as well as an additional set X as variables of sort dt. A state predicate ϕ ∈ F D A,X is to be interpreted over an A-data state ω and valuation β : X → D and we define the satisfaction relation

|= D by ω, β |= D A,X ϕ ⇐⇒ M, ι -1 M,dt • (ω ∪ β) |= Casl Sig(Dt),A∪X ϕ
where M ∈ Mod Casl (Dt) and ι M,dt : M(dt) ∼ = D. For a state predicate φ ∈ F D A,∅ not involving any variables, we write ω |= D

A φ for ω |= D A,∅ φ.

Example 7.3

The guard cnt + k ≤ 4 of the machine in Fig. 7.1 features both the attribute cnt and the variable k. A data state fulfilling this state predicate for k = 0 is cnt → 3.

Data transitions and effects.

A data transition (ω, ω ′ ) for a data signature A is a pair of A-data states; in particular, Ω 2 (A) = (D A ) 2 is the set of A-data transitions. It holds that (D A ) 2 ∼ = D 2A , where 2A = A ⊎ A and we assume that no attribute in A ends in a prime ′ and all attributes in the second summand are adorned with an additional prime. The effects of a machine are transition predicates in F 2D A,X = F D 2A,X . The satisfaction relation |= 2D for a transition predicate ψ ∈ F 2D A,X , data transition (ω, ω ′ ) ∈ Ω 2 (A), and valuation β : X → D is defined as

(ω, ω ′ ), β |= 2D A,X ψ ⇐⇒ ω + ω ′ , β |= D 2A,X ψ where ω + ω ′ ∈ Ω(2A) with (ω + ω ′ )(a) = ω(a) and (ω + ω ′ )(a ′ ) = ω ′ (a).
Example 7.4 The effect cnt ′ = cnt + k of the machine in Fig. 7.1 describes the increment of the value of attribute cnt by a variable amount k.

Syntax of Simple UML State Machines

A simple UML State Machine U uses an event/data signature Σ(U) for its events and attributes and consists of a finite set of control states C(U), a finite set of transition specifications T(U) of the form (c, ϕ, e(X), ψ, c ′ ) with c, c ′ ∈ C(U), e(X) ∈ E(Σ(U)), a state predicate ϕ ∈ F D A(Σ(U)),X , a transition predicate ψ ∈ F 2D A(Σ(U)),X , an initial control state c 0 (U) ∈ C(U), and an initial state predicate φ 0 (U) ∈ F D A(Σ(U)),∅ , such that C(U) is syntactically reachable, i.e., for every c ∈ C(U) \ {c 0 (U)} there are (c 0 (U), ϕ 1 , e 1 (X 1 ), ψ 1 , c 1 ), . . . , (c n-1 , ϕ n , e n (X n ), ψ n , c n ) ∈ T(U) with n > 0 such that c n = c. Syntactic reachability guarantees initially connected State Machine graphs. This simplifies graph-based algorithms (see Alg. 1).

In our input language, we will use different notations for guards and assignments. Guards we will write in the style expr1 == expr2. In assignments, instead of transition equations for attributes, we will write in the style attr1 := expr, which will then translate to the primed variant attr1 ′ = expr in the semantic notation and the translation to Casl.

Example 7.5 The machine in Fig. 7.1 has as its control states {s1, s2}, as its transition specifications {(s1, cnt + k ≤ 4, inc(k), cnt ′ = cnt + k, s1), (s1, cnt + k = 4, inc(k), cnt ′ = 4, s2), (s2, true, reset, cnt ′ = 0, s1)}, as initial control state s1, and as initial state predicate cnt = 0.

Event/Data Structures and Models of Simple UML State Machines

For capturing machines semantically, we use event/data structures that are given over an event/data signature Σ and consist of a transition system of configurations such that all configurations are reachable from its initial configurations. Herein, configurations show a control state, corresponding to machine states, and a data name from which a proper data state over A(Σ) can be retrieved by a labelling function. Transitions connect configurations by events from E(Σ) with their arguments instantiated by data from D.

Formally, a Σ-event/data structure M = (Γ, R, Γ 0 , ω) over an event/data signature Σ consists of a set of configurations Γ ⊆ C × D for some sets of control states C and data names D, a family of transition relations R = (R e(β) ⊆ Γ × Γ) e(X)∈E(Σ),β:X→D , and a non-empty set of initial configurations Γ 0 = {c 0 } × D 0 ⊆ Γ with a unique initial control state c 0 ∈ C such that Γ is reachable via R, i.e., for all γ ∈ Γ there are γ 0 ∈ Γ 0 , n ≥ 0, e 1 (X 1 ), . . . , e n (X n ) ∈ E(Σ), β 1 : X 1 → D, . . . , β n : X n → D, and (γ i , γ i+1 ) ∈ R e i+1 (β i+1 ) for all 0 ≤ i < n with γ n = γ; and a data state labelling ω : D → Ω(A(Σ)). We write c(M)(γ) = c and ω(M

)(γ) = ω(d) for γ = (c, d) ∈ Γ, Γ(M) for Γ, C(M) for {c(M)(γ) | γ ∈ Γ(M)}, R(M) for R, Γ 0 (M) for Γ 0 , c 0 (M) for c 0 , and Ω 0 (M) for {ω(M)(γ 0 ) | γ 0 ∈ Γ 0 }.
The restriction to reachable transition systems is not strictly necessary and could be replaced by constraining all statements on event/data structures to take into account only their reachable part (see, e.g., Lem. 7.11).

Example 7.6 For an event/data structure for the machine in Fig. 7.1 over its signature Σ in Ex. 7.1 we may choose the control states C as {s1, s2}, and the data names D as the set Ω(A(Σ)) = D {cnt} . In particular, the data state labelling ω is just the identity function. The only initial configuration is (s1, {cnt → 0}). A possible transition goes from configuration (s1, {cnt → 2}) to configuration (s2, {cnt → 4}) with the instantiated event inc(2).

A Σ(U)-event/data structure M is a model of a simple UML State Machine U if C(M) ⊇ C(U) up to a bijective renaming, c 0 (M) = c 0 (U), Ω 0 (M) ⊆ {ω ∈ |Ω(A(Σ(U)))| | ω |= D
A(Σ(U)) φ 0 (U)}, and if the following holds for all (c, d) ∈ Γ(M):

-for all (c, ϕ, e(X), ψ, c ′ ) ∈ T(U) and β :

X → D with ω(M)(d), β |= D A(Σ(U)),X ϕ, there is a ((c, d), (c ′ , d ′ )) ∈ R(M) e(β) with (ω(M)(d), ω(M)(d ′ )), β |= 2D A(Σ(U)),X ψ; -for all ((c, d), (c ′ , d ′ )) ∈ R(M) e(β)
there is either some (c, ϕ, e(X),

ψ, c ′ ) ∈ T(U) with ω(M)(d), β |= D A(Σ(U)),X ϕ and (ω(M)(d), ω(M)(d ′ )), β |= 2D A(Σ(U)),X ψ, or ω(M)(d), β ̸ |= D A(Σ(U)),X (c,ϕ,e(X),ψ,c ′ )∈T(U) ϕ, c = c ′ , and ω(M)(d) = ω(M)(d ′ ).
A model of U thus on the one hand implements each transition prescribed by U, but on the other hand must not show semantic transitions beyond those covered by the specified syntactic transitions. Moreover, it is input-enabled, i.e., every event can be consumed in every control state: If no precondition of an explicitly specified transition is satisfied, there is a self-loop which leaves the data state untouched. In fact, input-enabledness, as required by the UML specification [START_REF]Object Management Group. Unified Modeling Language[END_REF], can also be rendered as a syntactic transformation making a simple UML State Machine U input-enabled by adding the following set of transition specifications for idling self-loops:

{(c, ¬( (c,ϕ,e(X),ψ,c ′ )∈T(U) ϕ), e(X), 1 A(Σ(U)) , c) | c ∈ C, e(X) ∈ E(Σ(U)) } .
Example 7.7 For the simple UML State Machine in Fig. 7.1 the "grey" transitions correspond to an input-enabledness completion w.r.t. the "red" transitions.

Event/Data Signature Morphisms, Reducts, and Translations

The external interface of a simple UML State Machine is given by events, its internal interface by attributes. Both interfaces, represented as an event/data signature, are susceptible to change in the system development process which is captured by signature morphisms. Such changes must also be reflected in the guards and effects, i.e., data state and transition predicates, by syntactical translations as well as in the interpretation domains by semantical reducts.

A data signature morphism from a data signature A to a data signature A ′ is a function α : A → A ′ . The α-reduct of an A ′ -data state ω ′ : A ′ → D along a data signature morphism α : A → A ′ is given by the A-data state ω ′ |α : A → D with (ω ′ |α)(a) = ω ′ (α(a)) for every a ∈ A; the α-reduct of an A ′ -data transition (ω ′ , ω ′′ ) by the A-data transition (ω ′ , ω ′′ )|α = (ω ′ |α, ω ′′ |α). The state predicate translation F D α,X : F D A,X → F D A ′ ,X along a data signature morphism α : A → A ′ is given by the Casl-formula translation F Casl Sig(Dt),α∪1 X along the substitution α ∪ 1 X ; the transition predicate translation F 2D α,X by F D 2α,X with 2α : 2A → 2A ′ defined by 2α(a) = α(a) and 2α(a ′ ) = α(a) ′ . For each of these two reduct-translation-pairs the satisfaction condition holds due to the general substitution lemma for Casl:

ω ′ |α, β |= D A,X ϕ ⇐⇒ ω ′ , β |= D A ′ ,X F D α,X (ϕ) (ω ′ , ω ′′ )|α, β |= 2D A,X ψ ⇐⇒ (ω ′ , ω ′′ ), β |= 2D A ′ ,X F 2D α,X (ψ) An event signature morphism η : E → E ′ is a function η : |E| → |E ′ | such that υ(E)(e) = υ(E ′ )(η(e))
for all e ∈ |E|. An event/data signature morphism σ : Σ → Σ ′ consists of an event signature morphism E(σ) : E(Σ) → E(Σ ′ ) and a data signature morphism A(σ) :

A(Σ) → A(Σ ′ ). The σ-reduct of a Σ ′ -event/data structure M ′ along σ is the Σ-event/data structure M ′ |σ such that -the model components Γ(M ′ |σ) ⊆ Γ(M ′ ) and R(M ′ |σ) = (R(M ′ |σ) e(β)
) e(X)∈E(Σ),β:X→D are inductively defined by

• Γ(M ′ |σ) ⊇ Γ 0 (M ′ ) and • for all γ ′ , γ ′′ ∈ Γ(M ′ ), e(X) ∈ E(Σ), and β : X → D, if γ ′ ∈ Γ(M ′ |σ) and (γ ′ , γ ′′ ) ∈ R(M ′ ) E(σ)(e)(β) , then γ ′′ ∈ Γ(M ′ |σ) and (γ ′ , γ ′′ ) ∈ R(M ′ |σ) e(β) ; -Γ 0 (M ′ |σ) = Γ 0 (M ′ ); and -ω(M ′ |σ)(γ ′ ) = (ω(M ′ )(γ ′ ))|σ for all γ ′ ∈ Γ(M ′ |σ).
Building a reduct of an event/data-structure does not affect the single configurations, but potentially reduces the set of configurations by restricting the available events, and the data state observable from the data name of a configuration. We denote by Γ F (M, γ) and Γ F (M), respectively, the set of configurations of a Σ-event/data structure M that are F-reachable from a configuration γ ∈ Γ(M) and from an initial configuration γ 0 ∈ Γ 0 (M), respectively, with a set of events F ⊆ E(Σ) where a

γ n ∈ Γ(M) is F-reachable in M from a γ 1 ∈ Γ(M) if there are n ≥ 1, e 2 (X 2 ), . . . , e n (X n ) ∈ F, β 2 : X 2 → D, . . . , β n : X n → D, and (γ i , γ i+1 ) ∈ R(M) e i+1 (β i+1 ) for all 1 ≤ i < n.
Lemma 7.8 Let σ : Σ → Σ ′ be an event/data signature morphism, F ⊆ E(Σ), and M ′ a Σ ′ -event/data structure.

For all γ

′ 1 , γ ′ 2 ∈ Γ(M ′ ), if γ ′ 1 ∈ Γ(M ′ |σ), then (γ ′ 1 , γ ′ 2 ) ∈ R(M ′ |σ) e(β) if, and only if, (γ ′ 1 , γ ′ 2 ) ∈ R(M ′ ) E(σ)(e)(β) . 2. For all γ ′ , γ ′′ ∈ Γ(M ′ ) such that γ ′ ∈ Γ(M ′ |σ), γ ′′ ∈ Γ F (M ′ |σ, γ ′ ) if, and only if, γ ′′ ∈ Γ E(σ)(F) (M ′ , γ ′ ). 3. For all γ ′ ∈ Γ(M ′ ), γ ′ ∈ Γ F (M ′ |σ) if, and only if, γ ′ ∈ Γ E(σ)(F) (M ′ ).
Proof.

(1) This follows directly from the inductive definition of the σ-reduct of Σ ′ -event/data structures.

(

) Let γ ′ , γ ′′ ∈ Γ(M ′ ) with γ ′ ∈ Γ(M ′ |σ) 2
. By induction, it holds that γ ′′ ∈ Γ E(σ)(F) (M ′ ) if, and only if, there are n ≥ 0, e 1 (X 1 ), . . . , e n (X n ) ∈ F, and β 1 : X 1 → D, . . . , β n : X n → D, and

(γ ′ i , γ ′ i+1 ) ∈ R(M ′ ) E(σ)(e i+1 )(β i+1 ) for all 0 ≤ i < n with γ ′ = γ ′ 0 and γ ′′ = γ ′ n . Thus, by (1), since γ ′ ∈ Γ(M ′ |σ), γ ′′ ∈ Γ E(σ)(F) (M ′ ) if, and only if, γ ′′ ∈ Γ F (M ′ |σ). (3) Let γ ′ ∈ Γ(M ′ ). By definition it holds that γ ′ ∈ Γ E(σ)(F) (M ′ ) if, and only if, γ ′ ∈ Γ E(σ)(F) (M ′ , γ ′ 0 ) for some γ ′ 0 ∈ Γ 0 (M ′ ); if, and only if γ ′ ∈ Γ F (M ′ |σ, γ ′ 0 ) for some γ ′ 0 ∈ Γ(M ′ ) by (2) since γ ′ 0 ∈ Γ 0 (M ′ |σ); if, and only if, γ ′ ∈ Γ F (M ′ |σ) since Γ 0 (M ′ |σ) = Γ 0 (M ′ ).
Example 7.9 Let Σ be as in Ex. 7.1 and Σ 0 the event/data signature with E(Σ 0 ) = E(Σ) and A(Σ 0 ) = ∅. Consider the signature morphism σ : Σ 0 → Σ as the identity on the events and the trivial embedding on the attributes. Let M be a model of the simple UML State Machine in Fig. 7.1. The syntactic transition (s1, cnt + k ≤ 4, inc(k), cnt ′ = cnt + k, s1) induces, among others, the two semantic transitions ((s1, d 1 ), (s1, d 2 )), ((s1, d 2 ), (s1,

d 3 )) ∈ R(M) inc({k →1})
where ω(M)(d i ) = {cnt → i} for 1 ≤ i ≤ 3. In the reduct M|σ we find exactly these two semantic transitions, however, ω(M|σ)(d i ) = ∅ for all 1 ≤ i ≤ 3. This illustrates why we distinguish between data states and data names. With the distinction, we have a bijection between semantic transitions in the reduct and semantic transitions in the original structure. Without the distinction, the two different transitions in M would collapse into one transition only as there is just a single data state ∅.

Although it is straightforward to define a translation of simple UML State Machines along an event/data signature morphism, the rather restrictive notion of their models prevents the satisfaction condition from holding. In fact, this is already true for previous endeavours to institutionalise UML State Machines as part of this general research programme [KMRG15, KM17]. There, machines themselves were taken to be sentences over signatures comprising both events and states, and the satisfaction relation also required that a model should show exactly the transitions of such a machine sentence. For signature morphisms σ that are not surjective on states, building the reduct could result in fewer states and transitions, which leads to the same violation of the satisfaction condition which we found in [START_REF] Rosenberger | Relating UML state machines and interactions in an institutional framework[END_REF], shown here in Fig. 7.2.

We therefore propose to make a detour through a more general hybrid modal logic. This logic is directly based on event/data structures and thus close to the domain of State Machines. For forming an institution, its hybrid features allow to avoid control states as part of the signature and its event-based modalities allow to specify both mandatory and forbidden behaviour in a more fine-grained manner. Still, the logic is expressive enough to characterise the model class of a simple UML State Machine syntactically.

A Hybrid Modal Logic for Event/Data Systems

The logic EDHML is a hybrid modal logic for specifying event/data-based reactive systems and reasoning about them. The EDHML-signatures are the event/data signatures, the EDHMLstructures the event/data structures. The modal part of the logic allows to handle transitions between configurations where the modalities describe moves between configurations that adhere to a pre-condition or guard as a state predicate for an event with arguments and a transition predicate for the data change corresponding to effects. The hybrid part of the logic allows to bind control states of system configurations and to jump to configurations with such control states explicitly, but leaves out nominals as interfacing names as well as the possibility to quantify over control states. The logic builds on the hybrid dynamic logic D ↓ for specifying reactive systems without data [START_REF] Madeira | Dynamic Logic with Binders and Its Application to the Development of Reactive Systems[END_REF] and its extension E ↓ to handle also data [START_REF] Hennicker | A Hybrid Dynamic Logic for Event/Data-Based Systems[END_REF]. We restrict ourselves to modal operators consisting only of single instead of compound actions as done in dynamic logic. However, we still retain a box modality for accessing all configurations that are reachable from a given configuration. Moreover, we extend E ↓ by adding parameters to events.

The category of EDHML-signatures Sig EDHML consists of the event/data signatures and signature morphisms. The Σ-event/data structures form the discrete category Mod EDHML (Σ) of EDHML-structures over Σ. For each signature morphism σ :

Σ → Σ ′ in Sig EDHML the σ-reduct functor Mod EDHML (σ) : Mod EDHML (Σ ′ ) → Mod EDHML (Σ) is given by Mod EDHML (σ)(M ′ ) = M ′ |σ.
As the next step we introduce the formulae and sentences of EDHML together with their translation along Sig EDHML -morphisms and their satisfaction over Mod EDHML . We then show that for EDHML the satisfaction condition holds and thus obtain EDHML as an institution. Subsequently, we show that EDHML is expressive enough to characterise the model class of simple UML State Machines.

Formulae and Sentences of EDHML

EDHML-formulae aim at expressing control and data state properties of configurations as well as accessibility properties of configurations along transitions for particular events. The pure data state part is captured by data state sentences over D. The control state part can be accessed and manipulated by hybrid operators for binding the control state in a state variable, ↓s; checking for a particular control state, s; and accessing all configurations with a particular control state, @ F , which, however, only pertains to reachable configurations relative to a set F of events. Transitions between configurations are covered by different modalities: a box modality for accessing all configurations that are reachable from a given configuration, 2 F , again relative to a set F of events; a diamond modality for checking that an event with arguments is possible with a particular data state change, ⟨e(X) ψ⟩; and a modality for checking the reaction to an event with arguments according to a pre-condition and a transition predicate, ⟨|e(X) : ϕ ψ|⟩.

Formally, the Σ-event/data formulae F EDHML Σ,S over an event/data signature Σ and a set of state variables S are inductively defined by φ -data state sentence φ ∈ F D A(Σ),∅ holds in the current configuration;

s -the control state of the current configuration is s ∈ S;

-↓s . ϱ -calling the current control state s, formula ϱ ∈ F EDHML Σ,S⊎{s} holds;

-(@ F s)ϱ -in all configurations with control state s ∈ S that are reachable with events from F ⊆ E(Σ), the formula ϱ ∈ F EDHML Σ,S holds;

-2 F ϱ -in all configurations that are reachable from the current configuration with events from F ⊆ E(Σ) formula ϱ ∈ F EDHML Σ,S holds;

-⟨e(X) ψ⟩ϱ -in the current configuration there is a valuation of X and a transition for event e(X) ∈ E(Σ) with these arguments that satisfies transition formula ψ ∈ F 2D A(Σ),X and makes ϱ ∈ F EDHML Σ,S hold afterwards; -⟨|e(X) : ϕ ψ|⟩ϱ -in the current configuration for all valuations of X satisfying state formula ϕ ∈ F D A(Σ),X there is a transition for event e(X) ∈ E(Σ) with these arguments that satisfies transition formula ψ ∈ F 2D A(Σ),X and makes ϱ ∈ F EDHML Σ,S hold afterwards;

-¬ϱ -in the current configuration ϱ ∈ F EDHML Σ,S does not hold;

-

ϱ 1 ∨ ϱ 2 -in the current configuration ϱ 1 ∈ F EDHML Σ,S or ϱ 2 ∈ F EDHML Σ,S
hold.

We write (@s)ϱ for (@ E(Σ) s)ϱ, 2ϱ for 2 E(Σ) ϱ, 3 F ϱ for ¬2 F ¬ϱ, 3ϱ for 3 E(Σ) ϱ, [e(X) ψ]ϱ for ¬⟨e(X) ψ⟩¬ϱ, and true for ↓s . s.

Example 7.10 An event/data formula can make two kinds of requirements on an event/data structure: On the one hand, it can require the presence of certain mandatory transitions, on the other hand it can require the absence of certain prohibited transitions. Considering the simple UML State Machine in Fig. 7.1, the formula

(@s1)⟨|inc(k) : cnt + k = 4 cnt ′ = 4|⟩s2
requires for each valuation of β : {k} → N such that cnt + k = 4 holds that there is a transition from control state s1 to control state s2 for the instantiated event inc(β) where cnt is changed to 4. On the other hand, the formula

(@s2)[reset ¬(cnt ′ = 0)]false
prohibits any transitions out of s2 that are labelled with the event reset but do not satisfy cnt ′ = 0.

In the context of Fig. 7.1, these formulae only have their explained intended meaning when s1 and s2 indeed refer to the eponymous states. However, EDHML does not show nominals for explicitly naming control states as part of the State Machine's interface and the reference to specific states always has to build these states' context first using the modalities and the bind operator. On the other hand, as indicated in Sect. 7.2.4, the inclusion of nominals may interfere disadvantageously with the reduct formation.

Let σ : Σ → Σ ′ be an event/data signature morphism. The event/data formulae translation

F EDHML σ,S : F EDHML Σ,S → F EDHML Σ ′ ,S
along σ is recursively given by

-F EDHML σ,S (φ) = F D A(σ),∅ (φ); -F EDHML σ,S (s) = s; -F EDHML σ,S (↓s . ϱ) = ↓s . F EDHML σ,S⊎{s} (ϱ); -F EDHML σ,S ((@ F s)ϱ) = (@ E(σ)(F) s)F EDHML σ,S (ϱ)
;

-F EDHML σ,S (2 F ϱ) = 2 E(σ)(F) F EDHML σ,S (ϱ)
;

-F EDHML σ,S (⟨e(X) ψ⟩ϱ) = ⟨E(σ)(e)(X) F 2D A(σ),X (ψ)⟩F EDHML σ,S (ϱ)
;

-F EDHML σ,S (⟨|e(X) : ϕ ψ|⟩ϱ) = ⟨|E(σ)(e)(X) : F D A(σ),X (ϕ) F 2D A(σ),X (ψ)|⟩F EDHML σ,S (ϱ); -F EDHML σ,S (¬ϱ) = ¬F EDHML σ,S (ϱ); -F EDHML σ,S (ϱ 1 ∨ ϱ 2 ) = F EDHML σ,S (ϱ 1 ) ∨ F EDHML σ,S (ϱ 2 ).
The set Sen EDHML (Σ) of Σ-event/data sentences is given by F EDHML Σ,∅

, the event/data sentence translation Sen EDHML (σ) : Sen EDHML (Σ) → Sen EDHML (Σ ′ ) by F EDHML σ,∅ .

Satisfaction Relation for EDHML

The EDHML-satisfaction relation connects EDHML-structures and EDHML-formulae, expressing whether in some configuration of the structure a particular formula holds with respect to an assignment of control states to state variables. Let Σ be an event/data signature, M a Σ-event/data structure, S a set of state variables, v : S → C(M) a state variable assignment, and γ ∈ Γ(M). The satisfaction relation for event/data formulae is inductively given by

-M, v, γ |= EDHML Σ,S φ iff ω(M)(γ) |= D A(Σ) φ; -M, v, γ |= EDHML Σ,S s iff v(s) = c(M)(γ); -M, v, γ |= EDHML Σ,S ↓s . ϱ iff M, v{s → c(M)(γ)}, γ |= EDHML Σ,S⊎{s} ϱ; -M, v, γ |= EDHML Σ,S (@ F s)ϱ iff M, v, γ ′ |= EDHML Σ,S ϱ for all γ ′ ∈ Γ F (M) with c(M)(γ ′ ) = v(s); -M, v, γ |= EDHML Σ,S 2 F ϱ iff M, v, γ ′ |= EDHML Σ,S ϱ for all γ ′ ∈ Γ F (M, γ); -M, v, γ |= EDHML Σ,S ⟨e(X) ψ⟩ϱ iff there is a β : X → D and a γ ′ ∈ Γ(M) such that (γ, γ ′ ) ∈ R(M) e(β) , (ω(M)(γ), ω(M)(γ ′ )), β |= 2D A(Σ),X ψ, and M, v, γ ′ |= EDHML Σ,S ϱ; -M, v, γ |= EDHML Σ,S ⟨|e(X) : ϕ ψ|⟩ϱ iff for all β : X → D with ω(M)(γ), β |= D A(Σ),X ϕ there is some γ ′ ∈ Γ(M) such that (γ, γ ′ ) ∈ R(M) e(β) , (ω(M)(γ), ω(M)(γ ′ )), β |= 2D A(Σ),X ψ, and M, v, γ ′ |= EDHML Σ,S ϱ; -M, v, γ |= EDHML Σ,S ¬ϱ iff M, v, γ ̸ |= EDHML Σ,S ϱ; -M, v, γ |= EDHML Σ,S ϱ 1 ∨ ϱ 2 iff M, v, γ |= EDHML Σ,S ϱ 1 or M, v, γ |= EDHML Σ,S ϱ 2 .
This satisfaction relation is well-behaved with respect to reducts of EDHML-structures. On the one hand, this is due to the use of abstract data names rather than data states in the structures, and on the other hand, to the satisfaction condition of D and 2D. Lemma 7.11 Let σ : Σ → Σ ′ be an event/data signature morphism and M ′ a Σ ′ -event/data structure. For all ϱ ∈ F EDHML Σ,S , all γ ′ ∈ Γ(M ′ |σ) ⊆ Γ(M ′ ), and all v :

S → C(M ′ |σ) ⊆ C(M ′ ) it holds that M ′ |σ, v, γ ′ |= EDHML Σ,S ϱ ⇐⇒ M ′ , v, γ ′ |= EDHML Σ ′ ,S F EDHML σ,S (ϱ) .
Proof. We apply induction on the structure of Σ-event/data formulae.

Case φ:

M ′ |σ, v, γ ′ |= EDHML Σ,S φ ⇔ { def. |= EDHML } ω(M ′ |σ)(γ ′ ) |= D A(Σ) φ ⇔ { def. |σ } ω(M ′ )(γ ′ )|σ |= D A(Σ) φ ⇔ { sat. cond. D } ω(M ′ )(γ ′ ) |= D A(Σ ′ ) A(σ)(φ) ⇔ { def. |= EDHML } M ′ , v, γ ′ |= EDHML Σ ′ ,S A(σ)(φ) ⇔ { def. F EDHML σ,S } M ′ , v, γ ′ |= EDHML Σ ′ ,S F EDHML σ,S (φ) Case s: M ′ |σ, v, γ ′ |= EDHML Σ,S s ⇔ { def. |= EDHML } v(s) = c(M ′ |σ)(γ ′ ) ⇔ { def. |σ } v(s) = c(M ′ )(γ ′ ) ⇔ { def. |= EDHML } M ′ , v, γ ′ |= EDHML Σ ′ ,S s ⇔ { def. F EDHML σ,S } M ′ , v, γ ′ |= EDHML Σ ′ ,S F EDHML σ,S (s)
Case ↓s . ϱ:

M ′ |σ, v, γ ′ |= EDHML Σ,S ↓s . ϱ ⇔ { def. |= EDHML } M ′ |σ, v{s → c(M ′ |σ)(γ ′ )}, γ ′ |= EDHML Σ,S⊎{s} ϱ ⇔ { def. |σ and I. H. } M ′ , v{s → c(M ′ )(γ ′ )}, γ ′ |= EDHML Σ ′ ,S⊎{s} F EDHML σ,S⊎{s} (ϱ) ⇔ { def. |= EDHML } M ′ , v, γ ′ |= EDHML Σ ′ ,S ↓s . F EDHML σ,S⊎{s} (ϱ) ⇔ { def. F EDHML σ,S } M ′ , v, γ ′ |= EDHML Σ ′ ,S F EDHML σ,S (↓s . ϱ) Case (@ F s)ϱ: M ′ |σ, v, γ ′ |= EDHML Σ,S (@ F s)ϱ ⇔ { def. |= EDHML } M ′ |σ, v, γ ′′ |= EDHML Σ,S ϱ for all γ ′′ ∈ Γ F (M ′ |σ) with c(M ′ |σ)(γ ′′ ) = v(s) ⇔ { Lem. 7.8(3) } M ′ |σ, v, γ ′′ |= EDHML Σ,S ϱ for all γ ′′ ∈ Γ E(σ)(F) (M ′ ) with c(M ′ |σ)(γ ′′ ) = v(s) ⇔ { def. |σ and I. H. } M ′ , v, γ ′′ |= EDHML Σ ′ ,S F EDHML σ,S (ϱ) for all γ ′′ ∈ Γ E(σ)(F) (M ′ ) with c(M ′ )(γ ′′ ) = v(s) ⇔ { def. |= EDHML } M ′ , v, γ ′ |= EDHML Σ ′ ,S (@ E(σ)(F) s)F EDHML σ,S (ϱ) ⇔ { def. F EDHML σ,S } M ′ , v, γ ′ |= EDHML Σ ′ ,S F EDHML σ,S ((@ F s)ϱ) Case 2 F ϱ: M ′ |σ, v, γ ′ |= EDHML Σ,S 2 F ϱ ⇔ { def. |= EDHML } M ′ |σ, v, γ ′′ |= EDHML Σ,S ϱ for all γ ′′ ∈ Γ F (M ′ |σ, γ ′ ) ⇔ { Lem. 7.8(2) } M ′ |σ, v, γ ′′ |= EDHML Σ,S ϱ for all γ ′′ ∈ Γ E(σ)(F) (M ′ , γ ′ ) ⇔ { I. H. } M ′ , v, γ ′′ |= EDHML Σ ′ ,S F EDHML σ,S (ϱ) for all γ ′′ ∈ Γ E(σ)(F) (M ′ , γ ′ ) ⇔ { def. |= EDHML } M ′ , v, γ ′ |= EDHML Σ ′ ,S 2 E(σ)(F) F EDHML σ,S (ϱ) ⇔ { def. F EDHML σ,S } M ′ , v, γ ′ |= EDHML Σ ′ ,S F EDHML σ,S (2 F ϱ)
Case ⟨e(X) ψ⟩ϱ:

M ′ |σ, v, γ ′ |= EDHML Σ,S ⟨e(X) ψ⟩ϱ ⇔ { def. |= EDHML } M ′ |σ, v, γ ′′ |= EDHML Σ,S ϱ for some β : X → D, γ ′′ ∈ Γ(M ′ |σ) with (γ ′ , γ ′′ ) ∈ R(M ′ |σ) e(β) and (ω(M ′ |σ)(γ ′ ), ω(M ′ |σ)(γ ′′ )), β |= 2D A(Σ),X ψ ⇔ { Lem. 7.8(1) } M ′ |σ, v, γ ′′ |= EDHML Σ,S ϱ for some β : X → D, γ ′′ ∈ Γ(M ′ ) with (γ ′ , γ ′′ ) ∈ R(M ′ ) E(σ)(e)(β) and (ω(M ′ |σ)(γ ′ ), ω(M ′ |σ)(γ ′′ )), β |= 2D A(Σ),X ψ ⇔ { def. |σ } M ′ |σ, v, γ ′′ |= EDHML Σ,S ϱ for some β : X → D, γ ′′ ∈ Γ(M ′ ) with (γ ′ , γ ′′ ) ∈ R(M ′ ) E(σ)(e)(β) and (ω(M ′ )(γ ′ )|σ, ω(M ′ )(γ ′′ )|σ), β |= 2D A(Σ),X ψ ⇔ { sat. cond. 2D } M ′ |σ, v, γ ′′ |= EDHML Σ,S ϱ for some β : X → D, γ ′′ ∈ Γ(M ′ ) with (γ ′ , γ ′′ ) ∈ R(M ′ ) E(σ)(e)(β) and (ω(M ′ )(γ ′ ), ω(M ′ )(γ ′′ )), β |= 2D A(Σ ′ ),X F 2D A(σ),X (ψ) ⇔ { I. H. } M ′ , v, γ ′′ |= EDHML Σ ′ ,S F EDHML σ,S (ϱ) for some β : X → D, γ ′′ ∈ Γ(M ′ ) with (γ ′ , γ ′′ ) ∈ R(M ′ ) E(σ)(e)(β) and (ω(M ′ )(γ ′ ), ω(M ′ )(γ ′′ )), β |= 2D A(Σ ′ ),X F 2D A(σ),X (ψ) ⇔ { def. |= EDHML } M ′ , v, γ ′ |= EDHML Σ ′ ,S ⟨E(σ)(e)(X) F 2D A(σ),X (ψ)⟩F EDHML σ,S (ϱ) ⇔ { def. F EDHML σ,S } M ′ , v, γ ′ |= EDHML Σ ′ ,S F EDHML σ,S (⟨e(X) ψ⟩ϱ)
Case ⟨|e(X) : ϕ ψ|⟩ϱ:

M ′ |σ, v, γ ′ |= EDHML Σ,S ⟨|e(X) : ϕ ψ|⟩ϱ ⇔ { def. |= EDHML } M ′ |σ, v, γ ′′ |= EDHML Σ,S ϱ for all β : X → D such that ω(M ′ |σ)(γ ′ ), β |= D A(Σ),X ϕ and some γ ′′ ∈ Γ(M ′ |σ) with (γ ′ , γ ′′ ) ∈ R(M ′ |σ) e(β) and (ω(M ′ |σ)(γ ′ ), ω(M ′ |σ)(γ ′′ )), β |= 2D A(Σ),X ψ ⇔ { Lem. 7.8(1) } M ′ |σ, v, γ ′′ |= EDHML Σ,S ϱ for all β : X → D such that ω(M ′ |σ)(γ ′ ), β |= D A(Σ),X ϕ and some γ ′′ ∈ Γ(M ′ ) with (γ ′ , γ ′′ ) ∈ R(M ′ ) E(σ)(e)(β) and (ω(M ′ |σ)(γ ′ ), ω(M ′ |σ)(γ ′′ )), β |= 2D A(Σ),X ψ ⇔ { def. |σ } M ′ |σ, v, γ ′′ |= EDHML Σ,S ϱ for all β : X → D such that ω(M ′ )(γ ′ )|σ, β |= D A(Σ),X ϕ and some γ ′′ ∈ Γ(M ′ ) with (γ ′ , γ ′′ ) ∈ R(M ′ ) E(σ)(e)(β) and (ω(M ′ )(γ ′ )|σ, ω(M ′ )(γ ′′ )|σ), β |= 2D A(Σ),X ψ ⇔ { sat. cond. D, sat. cond. 2D } M ′ |σ, v, γ ′′ |= EDHML Σ,S ϱ for all β : X → D such that ω(M ′ )(γ ′ ), β |= D A(Σ ′ ),X F D A(σ),X (ϕ) and some γ ′′ ∈ Γ(M ′ ) with (γ ′ , γ ′′ ) ∈ R(M ′ ) E(σ)(e)(β) and (ω(M ′ )(γ ′ ), ω(M ′ )(γ ′′ )), β |= 2D A(Σ ′ ),X F 2D A(σ),X (ψ) ⇔ { I. H. } M ′ , v, γ ′′ |= EDHML Σ ′ ,S F EDHML σ,S (ϱ) for all β : X → D such that ω(M ′ )(γ ′ ), β |= D A(Σ ′ ),X F D A(σ),X (ϕ) and some γ ′′ ∈ Γ(M ′ ) with (γ ′ , γ ′′ ) ∈ R(M ′ ) E(σ)(e)(β) and (ω(M ′ )(γ ′ ), ω(M ′ )(γ ′′ )), β |= 2D A(Σ ′ ),X F 2D A(σ),X (ψ) ⇔ { def. |= EDHML } M ′ , v, γ ′ |= EDHML Σ ′ ,S ⟨|E(σ)(e)(X) : F D A(σ),X (ϕ) F 2D A(σ),X (ψ)|⟩F EDHML σ,S (ϱ) ⇔ { def. F EDHML σ,S } M ′ , v, γ ′ |= EDHML Σ ′ ,S F EDHML σ,S (⟨|e(X) : ϕ ψ|⟩ϱ)
Case ¬ϱ: ρ for all γ 0 ∈ Γ 0 (M).

M ′ |σ, v, γ ′ |= EDHML Σ,S ¬ϱ ⇔ { def. |= EDHML } M ′ |σ, v, γ ′ ̸ |= EDHML Σ,S ϱ ⇔ { I. H. } M ′ , v, γ ′ ̸ |= EDHML Σ ′ ,S F EDHML σ,S (ϱ) ⇔ { def. |= EDHML } M ′ , v, γ ′ |= EDHML Σ ′ ,S ¬F EDHML σ,S (ϱ) ⇔ { def. F EDHML σ,S } M ′ , v, γ ′ |= EDHML Σ ′ ,S F EDHML σ,S (¬ϱ) Case ϱ ∨ ς: M ′ |σ, v, γ ′ |= EDHML Σ,S ϱ ∨ ς ⇔ { def. |= EDHML } M ′ |σ, v, γ ′ |= EDHML Σ,S ϱ or M ′ |σ, v, γ ′ |= EDHML Σ,S ς ⇔ { I. H. } M ′ , v, γ ′ |= EDHML Σ ′ ,S F EDHML σ,S (ϱ) or M ′ , v, γ ′ |= EDHML Σ ′ ,S F EDHML σ,S (ς) ⇔ { def. |= EDHML } M ′ , v, γ ′ |= EDHML Σ ′ ,S F EDHML σ,S (ϱ) ∨ F EDHML σ,S (ς) ⇔ { def. F EDHML σ,S } M ′ , v, γ ′ |= EDHML Σ ′ ,S F EDHML σ,S (ϱ ∨ ς) For a Σ ∈ |Sig EDHML |, an M ∈ |Mod EDHML (Σ)|,
Theorem 7.12 (Sig EDHML , Mod EDHML , Sen EDHML , |= EDHML ) is an institution.

Proof. The satisfaction condition that for any

σ : Σ → Σ ′ in Sig EDHML , M ′ ∈ |Mod EDHML (Σ ′ )|, and ρ ∈ Sen EDHML (Σ), it holds that Mod EDHML (σ)(M ′ ) |= EDHML Σ ρ ⇐⇒ M ′ |= EDHML Σ ′ Sen EDHML (σ)(ρ)
directly follows from Lem. 7.11.

Alg. 1 Constructing an EDHML-sentence from a set of transition specifications

Require: T ≡ a set of transition specifications

Im T (c) = {(ϕ, e(X), ψ, c ′ ) | (c, ϕ, e(X), ψ, c ′ ) ∈ T} Im T (c, e(X)) = {(ϕ, ψ, c ′ ) | (c, φ, e(X), ψ, c ′ ) ∈ T} 1 function sen(c, I, V, B)
▷ c: state, I: image to visit, V: states to visit, B: bound states

2 if I ̸ = ∅ then 3 (ϕ, e(X), ψ, c ′ ) ← choose I 4 if c ′ ∈ B then 5 return (@c)⟨|e(X) : ϕ ψ|⟩(c ′ ∧ sen(c, I \ {(ϕ, e(X), ψ, c ′ )}, V, B)) 6 else 7 return (@c)⟨|e(X) : ϕ ψ|⟩(↓c ′ . sen(c, I \ {(ϕ, e(X), ψ, c ′ )}, V, B ∪ {c ′ })) 8 V ← V \ {c} 9 if V ̸ = ∅ then 10 c ′ ← choose B ∩ V 11 return sen(c ′ , Im T (c ′ ), V, B) 12 return ( c∈B fin(c)) ∧ c 1 ∈B,c 2 ∈B\{c 1 } ¬(@c 1 )c 2 13 function fin(c) 14 return (@c) e(X)∈E(Σ(U)) P⊆Im T (c,e(X)) [e(X) (ϕ,ψ,c ′ )∈P (ϕ ∧ ψ) ∧ ¬ (ϕ,ψ,c ′ )∈Im T (c,e(X))\P (ϕ ∧ ψ) ] (ϕ,ψ,c ′ )∈P c ′

Representing Simple UML State Machines in EDHML

The hybrid modal logic EDHML is expressive enough to characterise the model class of a simple UML State Machine U by a single sentence ϱ U , i.e., an event/data structure M is a model of U if, and only if, M |= EDHML Σ(U) ϱ U . Such a characterisation is achieved by means of Alg. 1 that is a slight variation of the characterisation algorithm for so-called operational specifications within E ↓ [HMK19] by including also events with data arguments. The algorithm constructs a sentence expressing that -all semantic transitions according to the explicit syntactic transition specifications are indeed possible and that -no further semantic transitions exist, i.e., every semantic transition adheres to some syntactic transition.

This sentence is expected to hold in the initial configuration and characterizes the entire machine. State names from the input are reused as variable names for control states. All state variables except the initial state are bound. Their distinctness is ensured (see the ¬(@c 1 )c 2 in Alg. 1). Together, this ensures state names can be consistently renamed, but are otherwise fixed.

The algorithm proceeds as follows: For a set of transition specifications T, a call sen(c, I, V, B) performs a recursive breadth-first traversal1 starting from c, where I holds the unprocessed quadruples2 (ϕ, e(X), ψ, c ′ ) of transitions in T outgoing from c, V the remaining states to visit, and B the set of already bound states. The function first requires the existence of each outgoing transition of I in the resulting formula, binding any newly reached state. Having visited all states in V, it requires that no other transitions from the states in B exist using calls to fin, and adds the requirement that all states in B are pairwise different. Formula fin(c) expresses that at c, for all events e(X) and for all subsets P of the transitions in T outgoing from c, whenever an e(X)-transition can be done with the combined effect of P but not adhering to any of the effects of the transitions currently not selected, the e(X)-transition must have one of the states as its target that are target states of P.

Example 7.13 Applying Alg. 1 to the set of explicitly mentioned, "red" transition specifications T of the simple UML State Machine Counter in Fig. 7.1, i.e., calling sen(s1, Im T (s1), {s1, s2}, {s1}) yields ϱ s1,s1 with

ϱ s1,s1 = (@s1)⟨|inc(k) : cnt + k ≤ 4 cnt ′ = cnt + k|⟩(s1 ∧ ϱ s1,s2 ) ϱ s1,s2 = (@s1)⟨|inc(k) : cnt + k = 4 cnt ′ = cnt + k|⟩↓s2 . (ϱ s2,s1 ) ϱ s2,s1 = (@s2)⟨|reset : true cnt ′ = 0|⟩(s1 ∧ ϱ fin ) ϱ fin = ϱ fin(s1) ∧ ϱ fin(s2) ∧ ¬(@s1)s2 ϱ fin(s1) = (@s1) [inc(k) ¬((cnt + k ≤ 4 ∧ cnt ′ = cnt + k) ∨ (cnt + k = 4 ∧ cnt ′ = 4))]false ∧ [inc(k) (cnt + k ≤ 4 ∧ cnt ′ = cnt + k) ∧ ¬(cnt + k = 4 ∧ cnt ′ = 4)]s1 ∧ [inc(k) (cnt + k = 4 ∧ cnt ′ = 4) ∧ ¬(cnt + k ≤ 4 ∧ cnt ′ = cnt + k)]s2 ∧ [inc(k) (cnt + k ≤ 4 ∧ cnt ′ = cnt + k) ∧ (cnt + k = 4 ∧ cnt ′ = 4)](s1 ∨ s2) ∧ [reset true]false ϱ fin(s2) = (@s2) [inc(k) true]false ∧ [reset ¬(cnt ′ = 0)]false ∧ [reset cnt ′ = 0]s1
In fact, there is no outgoing "red" transition for reset from s1, thus P = ∅ is the only choice for this event in fin(s1) and the clause [reset true]false is included. For inc(k) there are two outgoing transitions resulting in four different clauses checking whether none, the one or the other, or both transitions are executable.

In order to apply the algorithm to simple UML State Machines, the idling self-loops for achieving input-enabledness first have to be made explicit. For a syntactically input-enabled simple UML State Machine U a characterising sentence then reads

ϱ U = ↓c 0 . φ 0 ∧ sen(c 0 , Im T(U) (c 0 ), C(U), {c 0 }) ,
where c 0 = c 0 (U) and φ 0 = φ 0 (U). Due to syntactic reachability, the bound states B of Alg. 1 become C(U) when sen is called for B = {c 0 (U)} and V reaches ∅. In this chapter, we define a theoroidal comorphism from EDHML to Casl1. The construction mainly follows the standard translation of modal logics to first-order logic [START_REF] Goranko | Modal logic[END_REF] which has been considered for hybrid logics also on an institutional level [START_REF] Madeira | Foundations and Techniques for Software Reconfigurability[END_REF][START_REF] Diaconescu | Encoding Hybridized Institutions into First-order Logic[END_REF].

The contents of this chapter have appeared in similar form as part of our paper at WADT 2020 [START_REF] Rosenberger | Institution-based Encoding and Verification of Simple UML State Machines in CASL/SPASS[END_REF].

The construction of the comorphism was a common effort between Alexander Knapp, Markus Roggenbach and myself. In our virtual meetings, we jointly sketched the constructions, proofs and examples, which I then worked out in detail and wrote down in their final form.

Comorphism Definition

The basis is a representation of EDHML-signatures and the frame given by EDHML-structures as a Casl-specification as shown in Fig. 8.1. The signature translation ν Sig : Sig EDHML → Pres Casl maps an EDHML-signature Σ to the Casl-theory presentation given by Trans Σ and a EDHMLsignature morphism to the corresponding theory presentation morphism.

We will now give a line-by-line discussion of the translation frame in Fig. 8.1 for Trans Σ .

from Basic/StructuredDatatypes get Set % import finite sets spec Trans Σ = Dt then free type Evt ::= τ e (E(Σ)) -Trans Σ itself starts with a specification Dt of the underlying data universe.

% τ e ({e(X)}) = e(dt |X| ), τ e ({e(X)} ∪ E) = e(dt |X| ) | τ e (E) free type EvtNm ::= τ n (E(Σ)) % τ n ({e(X)}) = e, τ n ({e(X)} ∪ E) = e | τ n (E) op nm : Evt → EvtNm axiom ∀x 1 , . . . , x n : dt • nm(e(x 1 , . . . , x n )) = e % for each e(x 1 , . . . , x n ) ∈ E(Σ) then Set[sort EvtNm] then sort Ctrl free type Conf ::= conf(c : Ctrl; τ a (A(Σ))) % τ a ({a}) = a : dt, τ a ({a} ∪ A) = a : dt; τ a (A) preds init : Conf; trans : Conf × Evt × Conf • ∃g : Conf • init(g) % there is some initial configuration • ∀g, g ′ : Conf • init(g) ∧ init(g ′ ) ⇒ c(g) = c(g ′ ) % single initial control state free { pred reachable : Set[EvtNm] × Conf × Conf ∀g, g ′ , g ′′ : Conf, E : Set[EvtNm], e : Evt • reachable(E, g, g) • reachable(E, g, g ′ ) ∧ nm(e) ∈ E ∧ trans(g ′ , e, g ′′ ) ⇒ reachable(E, g, g ′′ ) } then preds reachable(E : Set[EvtName], g : Conf) ⇔ ∃g 0 : Conf • init(g 0 ) ∧ reachable(E, g 0 , g); reachable(g : Conf) ⇔ reachable(E(Σ), g) end
-Next, it introduces a free type Evt for events. The case distinction between the different event constructors is here generated by a meta-language function τ e , which recurses over the event set |E(Σ)| from the signature. For each event, we generate a constructor. To recall, each event e(X) comes with a finite set v(e(X)) of variables, which we here include as arguments to the event constructor.

-Next, we introduce the free type EvtNm for event names. The constructors are generated by the recursive function τ n , which is similar to τ e , but leaves out the arguments, i.e., an event name is an event without the data.

-Next, we include into Trans Σ the specification of finite sets, specialised to event names as elements.

-Next, we introduce a sort Ctrl for the control states.

-Next, we introduce a free type for configurations with only one constructor conf. A configuration is given by a control state and, for each attribute, one value from the data universe dt. The data value arguments to conf are generated by the function τ a , which recurses over the attribute set A(Σ) from the signature.

-Next, we introduce the predicate init which characterises initial configurations.

-Next, we introduce the transition predicate trans, which characterises triples of a configuration before the transition, an event and a configuration after the transition.

-Next, we require by an axiom that there is an initial configuration.

-Next, we require by an axiom that any two initial control states are equal.

-Next, we introduce the predicate reachable by a structured free block. In our experiments, we had to use different methods to encode the inductive nature of reachability, due to a lack of tools support for Casl's structured free construct. However, in the formal definition, we considered the structured free to be the clearest way of expressing what is going on here. In the structured free block we 1. introduce the predicate reachable, taking a set of event names (as we are considering reachability using only events with these names) and the configurations in which we start and end;

2. quantify over variables we will need in the following two axioms;

3. state the base case axioms, that each configuration is reachable from itself; and 4. state the step axiom, that transitions with allowed triggers preserve reachability.

-Finally, we introduce two abbreviated reachability predicates by first specialising the starting configuration to any allowed initial configuration, then by specialising the allowed set of event names to all event names from the signature.

The model translation

ν Mod Σ : Mod Casl (ν Sig (Σ)) → Mod EDHML (Σ)
can rely on the encoding just described. In particular, for a model M ′ ∈ Mod Casl (ν Sig (Σ)), there are, using the bijection ι M ′ ,dt :

dt M ′ ∼ = D, an injective map ι M ′ ,Conf : Conf M ′ ↣ Ctrl M ′ × Ω(A(Σ)) and a bijective map ι M ′ ,Evt : Evt M ′ ∼ = {e(β) | e(X) ∈ E(Σ), β : X → D}. The EDHML-structure resulting from a Casl-model of Trans Σ can thus be defined by -Γ(ν Mod Σ (M ′ )) = ι -1 M ′ ,Conf ({g ′ ∈ M ′ Conf | reachable M ′ (g ′ )}) -R(ν Mod Σ (M ′ )) e(β) = {(γ, γ ′ ) ∈ Γ(ν Mod Σ (M ′ )) × Γ(ν Mod Σ (M ′ )) | trans M ′ (ι M ′ ,Conf (γ), ι -1 M ′ ,Evt (e(β)), ι M ′ ,Conf (γ ′ ))}) -Γ 0 (ν Mod Σ (M ′ )) = {γ ∈ Γ(ν Mod Σ (M ′ )) | init M ′ (ι M ′ ,Conf (γ))}) -ω(ν Mod Σ (M ′ )) = {(c, ω) ∈ Γ(ν Mod Σ (M ′ )) → ω}
For EDHML-sentences, we first define a formula translation

ν F Σ,S,g : F EDHML Σ,S → F Casl ν Sig (Σ),S∪{g}
which, mimicking the standard translation, takes a variable g : Conf as a parameter that records the "current configuration" and also uses a set S of state names for the control states. The translation embeds the data state and 2-data state formulae using the substitution A(Σ)(g) = {a → a(g) | a ∈ A(Σ)} for replacing the attributes a ∈ A(Σ) by the accessors a(g). The translation of EDHML-formulae then reads

-ν F Σ,S,g (φ) = F Casl ν Sig (Σ),A(Σ)(g) (φ) -ν F Σ,S,g (s) = (s = c(g)) -ν F Σ,S,g (↓s . ϱ) = ∃s : Ctrl . s = c(g) ∧ ν F Σ,S⊎{s},g (ϱ) -ν F Σ,S,g ((@ F s)ϱ) = ∀g ′ : Conf . (c(g ′ ) = s ∧ reachable(F, g ′ )) ⇒ ν F Σ,S,g ′ (ϱ) -ν F Σ,S,g (2 F ϱ) = ∀g ′ : Conf . reachable(F, g, g ′ ) ⇒ ν F Σ,S,g ′ (ϱ) -ν F Σ,S,g (⟨e(X) ψ⟩ϱ) = ∃X : dt . ∃g ′ : Conf . trans(g, e(X), g ′ ) ∧ F Casl ν Sig (Σ),A(Σ)(g)∪A(Σ)(g ′ )∪1 X (ψ) ∧ ν F Σ,S,g ′ (ϱ) -ν F Σ,S,g (⟨|e(X) : ϕ ψ|⟩ϱ) = ∀X : dt . F Casl ν Sig (Σ),A(Σ)(g)∪1 X (ϕ) ⇒ ∃g ′ : Conf . trans(g, e(X), g ′ ) ∧ F Casl ν Sig (Σ),A(Σ)(g)∪A(Σ)(g ′ )∪1 X (ψ) ∧ ν F Σ,S,g ′ (ϱ) -ν F Σ,S,g (¬ϱ) = ¬ν F Σ,S,g (ϱ) -ν F Σ,S,g (ϱ 1 ∨ ϱ 2 ) = ν F Σ,S,g (ϱ 1 ) ∨ ν F Σ,S,g (ϱ 2 )
Example 8.1 The translation of (@s1)⟨|inc(x) : cnt + x ≤ 4 cnt ′ = cnt + x|⟩s1 over the state set {s1} and the configuration variable g is

ν F Σ,{s1},g ((@s1)⟨|inc(x) : cnt + x ≤ 4 cnt ′ = cnt + x|⟩s1) = ∀g ′ : Conf . (c(g ′ ) = s1 ∧ reachable(g ′ )) ⇒ ν F Σ,{s1},g ′ (⟨|inc(x) : cnt + x ≤ 4 cnt ′ = cnt + x|⟩s1) = ∀g ′ : Conf . (c(g ′ ) = s1 ∧ reachable(g ′ )) ⇒ ∀x : dt . cnt(g ′ ) + x ≤ 4 ⇒ ∃g ′′ : Conf . trans(g ′ , inc(x), g ′′ ) ∧ cnt(g ′′ ) = cnt(g ′ ) + x ∧ ν F Σ,{s1},g ′′ (s1) = ∀g ′ : Conf . (c(g ′ ) = s1 ∧ reachable(g ′ )) ⇒ ∀x : dt . cnt(g ′ ) + x ≤ 4 ⇒ ∃g ′′ : Conf . trans(g ′ , inc(x), g ′′ ) ∧ cnt(g ′′ ) = cnt(g ′ ) + x ∧ s1 = c(g ′′ )
Chapter 9

EDHMLO: Extending EDHML with Outputs In this chapter, we extend the institution and State Machine language from Chapter 7 with output events, thereby preparing the State Machines for Communication in the context of a Composite Structure. As a motivating example, Fig. 9.1 repeats the ATM system from the introduction, for we include a full specification parsable by our implementation in App. C and prove a safety property in Chapter 13.

In our architecture of communication, the queues are removed from machine configurations and treated instead in the Composite Structures. In the State Machines themselves, communication with the outside needs no handling beyond mentioning the messages in transitions; the existence of ports can largely be ignored by machines. This architecture means that, to handle communication on the State Machine side, we need only add output events. However, doing this in a way that respects the satisfaction condition is again somewhat involved, in particular, expressing the sets of input and output events in a context without full higher-order logic.

The contents of this chapter have been published in similar form as part of [START_REF] Rosenberger | An institutional approach to communicating UML State Machines[END_REF]. The construction of EDHMLO was a common effort between Alexander Knapp, Markus Roggenbach and myself. In our virtual meetings, we jointly sketched the constructions, proofs and examples, which I then worked out in detail and wrote down in their final form.

The Underlying Data Universe

We assume a consistent, monomorphic Casl specification Dt of data. The interpretation of the sorts S(Dt) of Dt represents the different kinds of data. In EDHML we had no need for such a type system. We do need it now because later, when we flatten Composite Structures, it will have to be possible for an attribute to contain a message queue or an entire submachine configuration. Requiring Dt to be monomorphic fixes the carrier sets as there is, up to isomorphism, a single model D of Dt. We also use open formulae F Casl Sig(Dt),X over sorted variables X = (X s ) s∈S(Dt) and their satisfaction relation D, β |= Casl Sig(Dt),X φ for a variable valuation β : X → D, i.e., β = (β s : X s → s D ) s∈S(Dt) .

Example 9.1 In our implementation, the State Machines themselves still use data signatures containing the natural numbers as the sole and implicit sort (richer data signatures will be needed to encode Composite Structures as Event/Data systems). A suitable specification for natural numbers would be the one from

Data States and Transitions

A data signature A consists of a finite set of attributes |A| and a sorting s(A) : |A| → S(Dt). A data signature morphism from a data signature A to a data signature A ′ is a function

α : |A| → |A ′ | such that s(A)(a) = s(A ′ )(α(a)
) for all a ∈ |A|. We sometimes identify A with the S(Dt)-sorted family (s(A) -1 (s)) s∈S(Dt) .

Example 9.2 A data signature for the ATM machine in Fig. 9.1 could be given by |A| = {trialsNum, cardId, pin} s(A)(x) = Nat for all x A data state ω for a data signature A is given by an attribute valuation ω : A → D, i.e., ω(a) ∈ s(A)(a) D for a ∈ |A|; in particular, Ω(A) = D A is the set of A-data states. The state predicates F D A,X are the formulae in F Casl Sig(Dt),A∪X , taking A as well as an additional S(Dt)-indexed family X as variables. A state predicate ϕ ∈ F D A,X is to be interpreted over an A-data state ω and variable valuation β : X → D and we define the satisfaction relation

|= D by ω, β |= D A,X ϕ ⇐⇒ D, ω ∪ β |= Casl Sig(Dt),A∪X ϕ . The α-reduct of an A ′ -data state ω ′ : A ′ → D along a data signature morphism α : A → A ′ is given by the A-data state ω ′ |α : A → D with (ω ′ |α)(a) = ω ′ (α(a)) for every a ∈ |A|. The state predicate translation F D α,X : F D A,X → F D A ′ ,X along α : A → A ′ is
given by the Caslformula translation F Casl Sig(Dt),α∪1 X along the substitution α ∪ 1 X . Reduct and translation fulfil the following satisfaction condition due to the general substitution lemma for Casl:

ω ′ |α, β |= D A,X ϕ ⇐⇒ ω ′ , β |= D A ′ ,X F D α,X (ϕ) .
A data transition (ω, ω ′ ) for a data signature A is a pair of A-data states; in particular, Ω 2 (A) = (D A ) 2 is the set of A-data transitions. It holds that (D A ) 2 ∼ = D 2A , where 2A = A ⊎ A and we assume that no attribute in A ends in a prime ′ and all attributes in the second summand are adorned with an additional prime. The transition predicates F 2D A,X are the formulae F D 2A,X . We will write cl A (ψ) for the transition predicate asserting that ψ holds and that all attributes a ∈ A not mentioned by ψ remain unchanged.

The satisfaction relation |= 2D for a transition predicate ψ ∈ F 2D A,X , data transition (ω, ω ′ ) ∈ Ω 2 (A), and valuation β : X → D is defined as

(ω, ω ′ ), β |= 2D A,X ψ ⇐⇒ ω + ω ′ , β |= D 2A,X ψ where ω + ω ′ ∈ Ω(2A) with (ω + ω ′ )(a) = ω(a) and (ω + ω ′ )(a ′ ) = ω ′ (a).
The α-reduct of an A ′ -data transition (ω ′ , ω ′′ ) along a data signature morphism α : A → A ′ is given by the A-data transition (ω ′ , ω ′′ )|α = (ω ′ |α, ω ′′ |α). The transition predicate translation F 2D α,X along α by F D 2α,X with 2α : 2A → 2A ′ defined by 2α(a) = α(a) and 2α(a ′ ) = α(a) ′ . Like for data states, reduct and translation fulfil the following satisfaction condition: The category of EDHMLO-signatures Sig EDHMLO consists of the event/data signatures and signature morphisms.

(ω ′ , ω ′′ )|α, β |= 2D A,X ψ ⇐⇒ (ω ′ , ω ′′ ), β |= 2D A ′ ,X F 2D α,X (ψ) .

Event/Data Structures

A configuration γ = (c, d) consists of -a control state c from some set of control states C and -a data state d from some set of data states D.

Given a data signature A the data state of γ may be labelled by a map ω such that ω(d) ∈ Ω(A). For a set of configurations Γ we write C(Γ) for its set of control states.

A Σ-event/data structure M = (Γ, R, Γ 0 , ω) over an event/data signature Σ consists of

-a set of configurations Γ ⊆ C × D, -a family of transition relations R = (R î, Ô ⊆ Γ × Γ) î∈ Î(Σ), Ô∈ Ô(Σ) * , and
-a non-empty set of initial configurations Γ 0 ⊆ Γ such that Γ is reachable from Γ 0 via R, i.e., for all γ ∈ Γ there are γ 0 ∈ Γ 0 , n ≥ 0, î1 , . . . , în ∈ Î(Σ), Ô1 , . . . , Ôn ∈ Ô(Σ) * , and (γ k , γ k+1 ) ∈ R îk+1 , Ôk+1 for all 0 ≤ k < n with γ n = γ;

and a data state labelling ω : D → Ω(A(Σ)). We write c(M)(γ) = c and ω(M

)(γ) = ω(d) for γ = (c, d) ∈ Γ, Γ(M) for Γ, C(M) for {c(M)(γ) | γ ∈ Γ(M)}, R(M) for R, Γ 0 (M) for Γ 0 , C 0 (M) for C(Γ 0 ), and Ω 0 (M) for {ω(M)(γ 0 ) | γ 0 ∈ Γ 0 }.
The above definition restricts structures to reachable ones only. This corresponds to our upcoming definition of the EDHMLO logic. In this logic, sentences will hold in a structure if they are satisfied in its initial states. However, using modalities, we still want to be able to express that a certain property holds for all states.

The σ-reduct of a Σ ′ -event/data structure M ′ along the event/data signature morphism

σ : Σ → Σ ′ is the Σ-event/data structure M ′ |σ such that -Γ(M ′ |σ) ⊆ Γ(M ′ ) as well as R(M ′ |σ) = (R(M ′ |σ) î, Ô) î∈ Î(Σ), Ô∈ Ô(Σ) * are inductively de- fined by Γ 0 (M ′ ) ⊆ Γ(M ′ |σ) and, for all γ ′ , γ ′′ ∈ Γ(M ′ ), î ∈ Î(Σ), and Ô ∈ Ô(Σ) * , if γ ′ ∈ Γ(M ′ |σ) and (γ ′ , γ ′′ ) ∈ R(M ′ ) Î(σ)(î), Ô(σ)( Ô) , then γ ′′ ∈ Γ(M ′ |σ) and (γ ′ , γ ′′ ) ∈ R(M ′ |σ) î, Ô; -Γ 0 (M ′ |σ) = Γ 0 (M ′ ); and -ω(M ′ |σ)(γ ′ ) = (ω(M ′ )(γ ′ ))|A(σ) for all γ ′ ∈ Γ(M ′ |σ).
This σ-reduct keeps exactly those transitions that are a direct image along σ. It would also be possible to additionally keep transitions that show a super-list of the outputs that can be reached by σ. When moving to EDHMLO sentences, however, it turns out to be impossible to fix a particular list of outputs.

Given sets of input events J ⊆ I(Σ) and output events N ⊆ O(Σ), we denote by Γ J,N (M, γ) and Γ J,N (M), respectively, the set of configurations of a Σ-event/data structure M that are J, N-reachable from a configuration γ ∈ Γ(M) and from an initial configuration γ 0 ∈ Γ 0 (M), respectively. Here a

γ n ∈ Γ(M) is J, N-reachable in M from a γ 1 ∈ Γ(M) if there are n ≥ 1, î2 , . . . , în ∈ Î(J), Ô2 , . . . , Ôn ∈ Ô(N) * , and (γ i , γ i+1 ) ∈ R(M) îk+1 , Ôk+1 for all 1 ≤ k < n.
The Σ-event/data structures form the discrete category Mod EDHMLO (Σ) of EDHMLO structures over Σ. For each σ :

Σ → Σ ′ in Sig EDHMLO the σ-reduct functor Mod EDHMLO (σ) : Mod EDHMLO (Σ ′ ) → Mod EDHMLO (Σ) is given by Mod EDHMLO (σ)(M ′ ) = M ′ |σ.

Event/Data Formulae and Sentences

The Σ-event/data formulae F EDHMLO Σ,S over an event/data signature Σ and a set of state variables S are inductively defined by φ -data state sentence φ ∈ F D A(Σ),∅ holds in the current configuration;

s -the control state of the current configuration is s ∈ S (unchanged compared to EDHML); -↓s . ϱ -calling the current control state s, formula ϱ ∈ F EDHMLO Σ,S⊎{s} holds; note that s is turned into a fresh variable by adding it with the disjoint sum operator to the set of state variables (unchanged compared to EDHML); -(@ J,N s)ϱ -in all configurations with control state s ∈ S that are J, N-reachable, formula ϱ ∈ F EDHMLO Σ,S holds (compared to EDHML, the output events N have been added here); -2 J,N ϱ -in all configurations that are J, N-reachable from the current configuration formula ϱ ∈ F EDHMLO Σ,S holds ('jump' operator; compared to EDHML, the output events N have been added here); -3i [O] N ψϱ -in the current configuration there are valuations β :

X(i) → D, β ′ : X(O) → D,
and a transition for the incoming message i(β) ∈ Î(Σ) and the outgoing messages

Ô′ ∈ O(β ′ ) ∥ N for O(β ′ ) ∈ Ô(Σ) * , N ∈ Ô(N) * such that β ∪ β ′ satisfies transition formula ψ ∈ F 2D A(Σ),X(i)∪X(O) and ϱ ∈ F EDHMLO Σ,S
holds afterwards (compared to EDHML, the stated (O) and ignored (N) output messages have been added); -⟨|i : ϕ [O] N : ψ|⟩ϱ -in the current configuration for all valuations β : X(i) → D satisfying state formula ϕ ∈ F D A(Σ),X(i) there are a valuation β ′ : X(O) → D and a transition for the incoming message i(β) ∈ Î(Σ) and the outgoing messages

Ô′ ∈ O(β ′ ) ∥ N for O(β ′ ) ∈ Ô(Σ) * , N ∈ Ô(N) * such that β ∪ β ′ satisfies transition formula ψ ∈ F 2D A(Σ),X(i)∪X(O) and ϱ ∈ F EDHMLO Σ,S
holds afterwards (compared to EDHML, the stated (O) and ignored (N) output messages have been added);

Event/Data Formulae and Sentences

-¬ϱ -in the current configuration ϱ ∈ F EDHMLO Σ,S does not hold (unchanged compared to EDHML);

-ϱ 1 ∨ ϱ 2 -in the current configuration ϱ 1 ∈ F EDHMLO Σ,S or ϱ 2 ∈ F EDHMLO Σ,S
holds (unchanged compared to EDHML).

We write (@s)ϱ for (@ I(Σ),O(Σ) s)ϱ, 2ϱ for 2 I(Σ),O(Σ) ϱ, 2i [O] N ψϱ for ¬3i [O] N ψ¬ϱ, and true for ↓s . s; we write O for [O] ∅ .

Two different kinds of relativisations are used in EDHMLO-formulae: For the jump operator (@ J,N s)ϱ and the always operator 2 J,N ϱ the subsets of input events J ⊆ I(Σ) and output events N ⊆ O(Σ) restrict the referrable states in an EDHMLO-structure to those that are J, N-reachable. Note that this information can be kept through translations to another EDHMLO-signature. On the other hand, [O] N specifies that besides messages from O additional messages for events in N ⊆ O(Σ) can be mixed into the output. However, in particular, [O] ∅ requires exactly O. The purpose of the relativisation [O] N is to specify with finitely many formulae (the set of output events is finite) to ignore message lists of arbitrary length.

Let σ : Σ → Σ ′ be an event/data signature morphism. The event/data formulae translation

F EDHMLO σ,S : F EDHMLO Σ,S → F EDHMLO Σ ′ ,S along σ is recursively given by -F EDHMLO σ,S (φ) = F D A(σ),∅ (φ)
;

-F EDHMLO σ,S (s) = s; -F EDHMLO σ,S (↓s . ϱ) = ↓s . F EDHMLO σ,S⊎{s} (ϱ); -F EDHMLO σ,S ((@ J,N s)ϱ) = (@ I(σ)(J),O(σ)(N) s)F EDHMLO σ,S (ϱ)
;

-F EDHMLO σ,S (2 J,N ϱ) = 2 I(σ)(J),O(σ)(N) F EDHMLO σ,S (ϱ)
;

-F EDHMLO σ,S (3i[O] N ψϱ) = 3I(σ)(i)[O(σ)(O)] O(σ)(N) F 2D A(σ),X(i)∪X(O) (ψ)F EDHMLO σ,S (ϱ)
;

-F EDHMLO σ,S (⟨|i : ϕ [O] N : ψ|⟩ϱ) = ⟨|I(σ)(i) : F D A(σ),X(i) (ϕ) [O(σ)(O)] O(σ)(N) : F 2D A(σ),X(i)∪X(O) (ψ)|⟩F EDHMLO σ,S (ϱ)
;

-F EDHMLO σ,S (¬ϱ) = ¬F EDHMLO σ,S (ϱ)
;

-F EDHMLO σ,S (ϱ 1 ∨ ϱ 2 ) = F EDHMLO σ,S (ϱ 1 ) ∨ F EDHMLO σ,S (ϱ 2 ).
The set Sen EDHMLO (Σ) of Σ-event/data sentences is given by

F EDHMLO Σ,∅
, the event/data sentence translation Sen EDHMLO (σ) : Sen EDHMLO

(Σ) → Sen EDHMLO (Σ ′ ) by F EDHMLO σ,∅ .
Example 9.4 In EDHMLO, just like in EDHML, we can express that a given class of transition must be possible, or that it must be impossible.

For the ATM machine in Fig. 9.1, we could have a set of state variables S = {cardId, pin, trialsNum}, the identity function as a state variable assignment v, as well as a data state d given by:

d : cardId → 7 pin → 42 trialsNum → 2
The transition from PINEntered to Verifying could be encoded in the following formula:

(@PINEntered)⟨|complOfATM.PINEntered : true [{bankCom.verify(cardId, pin)}] ∅ : cl A (true)|⟩CardEntered
This claims that in state PINEntered, there is a possible transition, regardless of the data state, which is triggered by the completion event for PINEntered1, and emitting exactly the event bankCom.verify, which is given as arguments the current values of cardId and pin. No data is changed, and the transition lands in the control state CardEntered.

Likewise, the transition from Verifying to CardEntered could be expressed by:

(@Verifying)⟨|bankCom.reenterPIN

: trialsNum < 3 [∅] ∅ : cl A (trialsNum ′ = trialsNum + 1) |⟩CardEntered
This asserts that in any configuration with control state Verifying, if trialsNum evaluates to a number strictly less than 3, then there is a transition with no outputs, increasing trialsNum by 1, leaving all other attributes unchanged and landing in control state CardEntered

Satisfaction Relation for EDHMLO

Let Σ be an event/data signature, M a Σ-event/data structure, S a set of state variables, v : S → C(M) a state variable assignment, and γ ∈ Γ(M). The satisfaction relation for event/data formulae is inductively given by

-M, v, γ |= EDHMLO Σ,S φ iff ω(M)(γ), ∅ |= D A(Σ),∅ φ; -M, v, γ |= EDHMLO Σ,S s iff v(s) = c(M)(γ); -M, v, γ |= EDHMLO Σ,S ↓s . ϱ iff M, v{s → c(M)(γ)}, γ |= EDHMLO Σ,S⊎{s} ϱ; -M, v, γ |= EDHMLO Σ,S (@ J,N s)ϱ iff M, v, γ ′ |= EDHMLO Σ,S ϱ for all γ ′ ∈ Γ J,N (M) with c(M)(γ ′ ) = v(s); -M, v, γ |= EDHMLO Σ,S 2 J,N ϱ iff M, v, γ ′ |= EDHMLO Σ,S
ϱ for all γ ′ ∈ Γ J,N (M, γ); 1 The completion event is delivered over a special internal port for completion events 106 9.8. Satisfaction Condition ρ for all γ 0 ∈ Γ 0 (M).

-M, v, γ |= EDHMLO Σ,S 3i[O] N ψϱ iff there are valuations β : X(i) → D, β ′ : X(O) → D, output messages Ô′ ∈ O(β ′ ) ∥ N with N ∈ Ô(N) * , and a configuration γ ′ ∈ Γ(M) such that (γ, γ ′ ) ∈ R(M) i(β), Ô′ , (ω(M)(γ), ω(M)(γ ′ )), β ∪ β ′ |= 2D A(Σ),X(i)∪X(O) ψ, and M, v, γ ′ |= EDHMLO Σ,S ϱ; -M, v, γ |= EDHMLO Σ,S ⟨|i : ϕ [O] N : ψ|⟩ϱ iff for all valuations β : X(i) → D that satisfy ω(M)(γ), β |= D A(Σ),X(i) ϕ there are a valuation β ′ : X(O) → D, output messages Ô′ ∈ O(β ′ ) ∥ N with N ∈ Ô(N) * , and a configuration γ ′ ∈ Γ(M) such that (γ, γ ′ ) ∈ R(M) i(β), Ô′ , (ω(M)(γ), ω(M)(γ ′ )), β ∪ β ′ |= 2D A(Σ),X(i)∪X(O) ψ, and M, v, γ ′ |= EDHMLO Σ,S ϱ; -M, v, γ |= EDHMLO Σ,S ¬ϱ iff M, v, γ ̸ |= EDHMLO Σ,S ϱ; -M, v, γ |= EDHMLO Σ,S ϱ 1 ∨ ϱ 2 iff M, v, γ |= EDHMLO Σ,S ϱ 1 or M, v, γ |= EDHMLO Σ,S ϱ 2 .
Example 9.5 For the ATM machine in Fig. 9.1, we could again have the set of state variables S = {cardId, pin, trialsNum}, the identity function as a state variable assignment v, as well as the data state d given by:

d : cardId → 7 pin → 42 trialsNum → 2
Then, the satisfaction of the transition formula from Verifying to CardEntered in the configuration γ = (Verifying, d) would be expressed as:

(Γ, R, Γ 0 , ω), v, γ |= EDHMLO Σ,S (@Verifying)⟨|bankCom.reenterPIN : trialsNum < 3 [∅] ∅ : cl A (trialsNum ′ = trialsNum + 1) |⟩CardEntered
This would hold iff (γ, (CardEntered, d{trialsNum → 3})) ∈ R bankCom.reenterPIN,∅ .

Satisfaction Condition

Theorem 9.6 (Sig EDHMLO , Mod EDHMLO , Sen EDHMLO , |= EDHMLO ) is an institution.

Proof. The satisfaction condition for sentences follows directly from that for formulae, i.e., for signature morphisms σ : Σ → Σ ′ , models M ′ ∈ |Mod EDHMLO (Σ ′ )|, state variables S, state variable assignments v : S → C(M ′ ), configurations γ ∈ Γ(M) and formulae F EDHMLO Σ,S , we have to show that

M ′ |σ, v, γ |= EDHMLO Σ,S ϱ is equivalent to M ′ , v, γ |= EDHMLO Σ ′ ,S F EDHMLO σ,S (ϱ).
We prove this by structural induction over ϱ. Case φ:

M ′ |σ, v, γ |= EDHMLO Σ,S φ ⇔ { def. |= EDHMLO } ω(M)(γ), ∅ |= D A(Σ),∅ φ; ⇔ { def. |σ } ω(M ′ )(γ ′ )|σ |= D A(Σ),∅ φ ⇔ { sat. cond. D } ω(M ′ )(γ ′ ) |= D A(Σ ′ ),∅ A(σ)(φ) ⇔ { def. |= EDHMLO } M ′ , v, γ ′ |= EDHMLO Σ ′ ,S A(σ)(φ) ⇔ { def. F EDHMLO σ,S } M ′ , v, γ |= EDHMLO Σ ′ ,S F EDHMLO σ,S (φ) Case s: M ′ |σ, v, γ ′ |= EDHMLO Σ,S s ⇔ { def. |= EDHMLO } v(s) = c(M ′ |σ)(γ ′ ) ⇔ { def. |σ } v(s) = c(M ′ )(γ ′ ) ⇔ { def. |= EDHMLO } M ′ , v, γ ′ |= EDHMLO Σ ′ ,S s ⇔ { def. F EDHMLO σ,S } M ′ , v, γ ′ |= EDHMLO Σ ′ ,S F EDHMLO σ,S (s) Case ↓s . ϱ: M ′ |σ, v, γ ′ |= EDHMLO Σ,S ↓s . ϱ ⇔ { def. |= EDHMLO } M ′ |σ, v{s → c(M ′ |σ)(γ ′ )}, γ ′ |= EDHMLO Σ,S⊎{s} ϱ ⇔ { def. |σ and I. H. } M ′ , v{s → c(M ′ )(γ ′ )}, γ ′ |= EDHMLO Σ ′ ,S⊎{s} F EDHMLO σ,S⊎{s} (ϱ) ⇔ { def. |= EDHMLO } M ′ , v, γ ′ |= EDHMLO Σ ′ ,S ↓s . F EDHMLO σ,S⊎{s} (ϱ) ⇔ { def. F EDHMLO σ,S } M ′ , v, γ ′ |= EDHMLO Σ ′ ,S F EDHMLO σ,S (↓s . ϱ)
Case (@ J,N s)ϱ:

M ′ |σ, v, γ ′ |= EDHMLO Σ,S (@ J,N s)ϱ ⇔ { def. |= EDHMLO } M ′ |σ, v, γ ′′ |= EDHMLO Σ,S ϱ for all γ ′′ ∈ Γ J,N (M ′ |σ) with c(M ′ |σ)(γ ′′ ) = v(s) ⇔ { def. |σ; Γ reachable from Γ 0 via R } M ′ |σ, v, γ ′′ |= EDHMLO Σ,S ϱ for all γ ′′ ∈ Γ I(σ)(J),O(σ)(N) (M ′ ) with c(M ′ |σ)(γ ′′ ) = v(s) ⇔ { I. H. } M ′ , v, γ ′′ |= EDHMLO Σ,S F EDHMLO σ,S (ϱ) for all γ ′′ ∈ Γ I(σ)(J),O(σ)(N) (M ′ ) with c(M ′ )(γ ′′ ) = v(s) ⇔ { def. |= EDHMLO } M ′ , v, γ ′ |= EDHMLO Σ ′ ,S (@ I(σ)(J),O(σ)(N) s)F EDHMLO σ,S (ϱ) ⇔ { def. F EDHMLO σ,S } M ′ , v, γ ′ |= EDHMLO Σ ′ ,S F EDHMLO σ,S ((@ J,N s)ϱ) Case 2 J,N ϱ: M ′ |σ, v, γ ′ |= EDHMLO Σ,S 2 J,N ϱ ⇔ { def. |= EDHMLO } M ′ |σ, v, γ ′′ |= EDHMLO Σ,S ϱ for all γ ′′ ∈ Γ J,N (M ′ |σ, γ ′ ) ⇔ { def. |σ; Γ reachable from Γ 0 via R } M ′ |σ, v, γ ′′ |= EDHMLO Σ,S ϱ for all γ ′′ ∈ Γ I(σ)(J),O(σ)(N) (M ′ |σ, γ ′ ) ⇔ { I. H. } M ′ , v, γ ′′ |= EDHMLO Σ ′ ,S F EDHMLO σ,S (ϱ) for all γ ′′ ∈ Γ I(σ)(J),O(σ)(N) (M ′ , γ ′ ) ⇔ { def. |= EDHMLO } M ′ , v, γ ′ |= EDHMLO Σ ′ ,S 2 J,N F EDHMLO σ,S (ϱ) ⇔ { def. F EDHMLO σ,S } M ′ , v, γ ′ |= EDHMLO Σ ′ ,S F EDHMLO σ,S (2 J,N ϱ) Case 3i[O] N ψϱ: M ′ |σ, v, γ ′ |= EDHMLO Σ,S 3i[O] N ψϱ ⇔ { def. |= EDHMLO } M ′ |σ, v, γ ′′ |= EDHMLO Σ,S ϱ for some β : X(i) → D, β ′ : X(O) → D, Ô′ ∈ O(β ′ ) ∥ N with N ∈ Ô(N) * , γ ′′ ∈ Γ(M ′ |σ) and (γ ′ , γ ′′ ) ∈ R(M ′ |σ) i(β), Ô′ with (ω(M ′ |σ)(γ ′ ), ω(M ′ |σ)(γ ′′ )), β ∪ β ′ |= 2D A(Σ),X(i)∪X(O) ψ ⇔ { event signature morphism preserve parameter sorts } M ′ |σ, v, γ ′′ |= EDHMLO Σ,S ϱ for some β : X(I(σ)(i)) → D, β ′ : X(O(σ)(O)) → D, Ô′ ∈ O(β ′ ) ∥ N with N ∈ Ô(N) * , γ ′′ ∈ Γ(M ′ |σ) and (γ ′ , γ ′′ ) ∈ R(M ′ |σ) i(β), Ô′ with (ω(M ′ |σ)(γ ′ ), ω(M ′ |σ)(γ ′′ )), β ∪ β ′ |= 2D A(Σ),X(i)∪X(O) ψ ⇔ { def. |σ; Γ reachable from Γ 0 via R } M ′ |σ, v, γ ′′ |= EDHMLO Σ,S ϱ for some β : X(I(σ)(i)) → D, β ′ : X(O(σ)(O)) → D, Ô′ ∈ O(σ)(O)(β ′ ) ∥ N with N ∈ Ô(N) * , γ ′′ ∈ Γ(M ′ |σ) and (γ ′ , γ ′′ ) ∈ R(M ′ ) I(σ)(i)(β), Ô′ with (ω(M ′ |σ)(γ ′ ), ω(M ′ |σ)(γ ′′ )), β ∪ β ′ |= 2D A(Σ),X(i)∪X(O) ψ ⇔ { sat. cond. 2D } M ′ |σ, v, γ ′′ |= EDHMLO Σ,S ϱ for some β : X(I(σ)(i)) → D, β ′ : X(O(σ)(O)) → D, Ô′ ∈ O(σ)(O)(β ′ ) ∥ N with N ∈ Ô(N) * , γ ′′ ∈ Γ(M ′ |σ) and (γ ′ , γ ′′ ) ∈ R(M ′ ) I(σ)(i)(β), Ô′ with (ω(M ′ )(γ), ω(M ′ )(γ ′ )), β ∪ β ′ |= 2D A(Σ),X(i)∪X(O) F 2D A(σ),X (ψ) ⇔ { I. H. } M ′ , v, γ ′′ |= EDHMLO Σ ′ ,S 3I(σ(i)[O(σ)(O)] O(σ)(N) ψF EDHMLO σ,S (ϱ) for some β : X(I(σ(i)) → D, β ′ : X(O(σ)(O)) → D, Ô′ ∈ O(σ)(O(β ′ ) ∥ N with N ∈ Ô(N) * , γ ′′ ∈ Γ(M ′ ) and (γ ′ , γ ′′ ) ∈ R(M ′ ) I(σ)(i)(β), Ô′ with (ω(M ′ |σ)(γ ′ ), ω(M ′ )(γ ′′ )), β ∪ β ′ |= 2D A(Σ),X(i)∪X(O) ψ ⇔ { def. |= EDHMLO } M ′ , v, γ ′ |= EDHMLO Σ ′ ,S 3I(σ(i)[O(σ)(O)] N ψF EDHMLO σ,S (ϱ) ⇔ { def. F EDHMLO σ,S } M ′ , v, γ ′ |= EDHMLO Σ ′ ,S F EDHMLO σ,S (3i[O] N ψϱ) Case ⟨|i : ϕ [O] N : ψ|⟩ϱ: M ′ |σ, v, γ ′ |= EDHMLO Σ,S ⟨|i : ϕ [O] N : ψ|⟩ϱ ⇔ { def. |= EDHMLO } M ′ |σ, v, γ ′′ |= EDHMLO Σ ′ ,S ⟨|i : σ, X(i) ϕ : [O] N |⟩ψϱ for all β : X(i) → D satisfying ω(M ′ |σ)(γ), β |= D A(Σ),X(i) ϕ and some β ′ : X(O) → D, Ô′ ∈ O(β ′ ) ∥ N with N ∈ Ô(N) * , γ ′′ ∈ Γ(M ′ ) and (γ ′ , γ ′′ ) ∈ R(M ′ |σ) i(β), Ô′ with (ω(M ′ |σ)(γ ′ ), ω(M ′ |σ)(γ ′′ )), β ∪ β ′ |= 2D A(Σ),X(i)∪X(O) ψ ⇔ { event signature morphism preserve parameter sorts } M ′ |σ, v, γ ′′ |= EDHMLO Σ ′ ,S ⟨|i : F D σ,A(σ),X(i) (ϕ) [O(σ)(O)] N : F 2D σ,A(σ),X(i) (ψ)|⟩ϱ for all β : X(I(σ(i)) → D satisfying ω(M ′ )(γ)|A(σ), β |= D A(Σ),X(i) ϕ and some β ′ : X(O(σ)(O)) → D, Ô(σ)(O) ′ ∈ O(σ)(O(β ′ ) ∥ N with N ∈ Ô(N) * , γ ′′ ∈ Γ(M ′ ) and (γ ′ , γ ′′ ) ∈ R(M ′ |σ) i(β), Ô′ with (ω(M ′ )(γ ′ )|A(σ), ω(M ′ )(γ ′′ )|A(σ)), β ∪ β ′ |= 2D A(Σ),X(i)∪X(O(σ)(O)) ψ ⇔ { def. |σ; Γ reachable from Γ 0 via R } M ′ |σ, v, γ ′′ |= EDHMLO Σ ′ ,S ⟨|i : F D σ,A(σ),X(i) (ϕ) [O(σ)(O)] N : F 2D σ,A(σ),X(i) (ψ)|⟩ϱ for all β : X(I(σ(i)) → D satisfying ω(M ′ )(γ)|A(σ), β |= D A(Σ),X(i) ϕ and some β ′ : X(O(σ)(O)) → D, Ô(σ)(O) ′ ∈ O(σ)(O(β ′ ) ∥ N with N ∈ Ô(N) * , γ ′′ ∈ Γ(M ′ ) and (γ ′ , γ ′′ ) ∈ R(M ′ ) I(σ)(i)(β), Ô(σ)(O) ′ with (ω(M ′ )(γ ′ )|A(σ), ω(M ′ )(γ ′′ )|A(σ)), β ∪ β ′ |= 2D A(Σ),X(i)∪X(O(σ)(O)) ψ ⇔ { sat. cond. 2D; sat. cond. 2D } M ′ |σ, v, γ ′′ |= EDHMLO Σ,S ⟨|i : F D σ,A(σ),X(i) (ϕ) [O(σ)(O)] N : F 2D σ,A(σ),X(i) (ψ)|⟩ϱ for all β : X(I(σ(i)) → D satisfying ω(M ′ )(γ), β |= D A(Σ ′ ),X(i) F D σ,A(σ),X(i) (ϕ) and some β ′ : X(O(σ)(O)) → D, Ô(σ)(O) ′ ∈ O(σ)(O(β ′ ) ∥ N with N ∈ Ô(N) * , γ ′′ ∈ Γ(M ′ ) and (γ ′ , γ ′′ ) ∈ R(M ′ ) I(σ)(i)(β), Ô(σ)(O) ′ with (ω(M ′ )(γ ′ ), ω(M ′ )(γ ′′ )), β ∪ β ′ |= 2D A(Σ ′ ),X(i)∪X(O(σ)(O)) F 2D σ,A(σ),X(i) (ψ) ⇔ { I. H. } M ′ , v, γ ′′ |= EDHMLO Σ ′ ,S ⟨|i : F D σ,A(σ),X(i) (ϕ) [O(σ)(O)] N : F 2D σ,A(σ),X(i) (ψ)|⟩F EDHMLO σ,S (ϱ)
for all β :

X(I(σ(i)) → D satisfying ω(M ′ )(γ), β |= D A(Σ ′ ),X(i) F D σ,A(σ),X(i) (ϕ) and some β ′ : X(O(σ)(O)) → D, Ô(σ)(O) ′ ∈ O(σ)(O(β ′ ) ∥ N with N ∈ Ô(N) * , γ ′′ ∈ Γ(M ′ ) and (γ ′ , γ ′′ ) ∈ R(M ′ ) I(σ)(i)(β), Ô(σ)(O) ′ with (ω(M ′ )(γ ′ ), ω(M ′ )(γ ′′ )), β ∪ β ′ |= 2D A(Σ ′ ),X(i)∪X(O(σ)(O)) F 2D σ,A(σ),X(i) (ψ) ⇔ { def. |= EDHMLO } M ′ , v, γ ′ |= EDHMLO Σ ′ ,S ⟨|I(σ)(i) : F D σ,A(σ),X(i) (ϕ) [O(σ)(O)] N) : F 2D σ,A(σ),X(i) (ψ)|⟩F EDHMLO σ,S (ϱ) ⇔ { def. F EDHMLO σ,S } M ′ , v, γ ′ |= EDHMLO Σ ′ ,S F EDHMLO σ,S (⟨|i : ϕ [O] N : ψ|⟩ϱ)
Case ¬ϱ: In this chapter, we present a notion of simple UML Composite Structures built on EDHMLO.

M ′ |σ, v, γ ′ |= EDHMLO Σ,S ¬ϱ ⇔ { def. |= EDHMLO } M ′ |σ, v, γ ′ ̸ |= EDHMLO Σ,S ϱ ⇔ { I. H. } M ′ , v, γ ′ ̸ |= EDHMLO Σ ′ ,S F EDHMLO σ,S (ϱ) ⇔ { def. |= EDHMLO } M ′ , v, γ ′ |= EDHMLO Σ ′ ,S ¬F EDHMLO σ,S (ϱ) ⇔ { def. F EDHMLO σ,S } M ′ , v, γ ′ |= EDHMLO Σ ′ ,S F EDHMLO σ,S (¬ϱ) Case ϱ ∨ ς: M ′ |σ, v, γ ′ |= EDHMLO Σ,S ϱ ∨ ς ⇔ { def. |= EDHMLO } M ′ |σ, v, γ ′ |= EDHMLO Σ,S ϱ or M ′ |σ, v, γ ′ |= EDHMLO Σ,S ς ⇔ { I. H. } M ′ , v, γ ′ |= EDHMLO Σ ′ ,S F EDHMLO σ,S (ϱ) or M ′ , v, γ ′ |= EDHMLO Σ ′ ,S F EDHMLO σ,S (ς) ⇔ { def. |= EDHMLO } M ′ , v, γ ′ |= EDHMLO Σ ′ ,S F EDHMLO σ,S (ϱ) ∨ F EDHMLO σ,S (ς) ⇔ { def. F EDHMLO σ,S } M ′ , v, γ ′ |= EDHMLO Σ ′ ,S
The contents of this chapter have been published in similar form as part of [START_REF] Rosenberger | An institutional approach to communicating UML State Machines[END_REF]. They result from a common effort between Alexander Knapp, Markus Roggenbach and myself. In our virtual meetings, we jointly sketched the constructions, proofs and examples, which I then worked out in detail and wrote down in their final form.

Signatures

A UML Composite Structure specifies the internal structure and external connections of a class or component. For our purposes, a Composite Structure is given by class or component instances, its so-called parts, that can communicate through their attached ports specifying input and output interfaces and being linked by connectors. All connectors are assumed to be binary and each part to be equipped with a State Machine for describing its behaviour.

A Composite Structure signature ∆ over EDHMLO consists of -for each connection (p, p ′ ) ∈ Con(∆), the output events of port p are input events for port p ′ , i.e., O(Sig(∆, p)) ⊆ I(Sig(∆, p ′ )).

We say that port The signature for the atm component could be given by the following input events, output events and attributes:

p ∈ Prt(∆) is open in ∆ if there is no p ′ ∈ Prt(∆) such that (p, p ′ ) ∈ Con(∆); otherwise p is connected. A Composite Structure signature morphism δ : ∆ → ∆ ′ over EDHMLO consists of
∆ ′ is computed componentwise as (C ′ (Cmp(δ)(c))|Sig(δ, c)) c∈Cmp(∆) . The ∆-Composite
Structure structures form the discrete category Mod cs(EDHMLO) (∆) of cs(EDHMLO)-structures over ∆. For each signature morphism δ : ∆ → ∆ ′ in Sig cs(EDHMLO) the δ-reduct functor

Mod cs(EDHMLO) (δ) : Mod cs(EDHMLO) (∆ ′ ) → Mod cs(EDHMLO) (∆) is given by Mod cs(EDHMLO) (δ)(C ′ ) = C ′ |δ.
In UML, State Machines organised in a Composite Structure communicate with each other by sending messages which are stored in event pools. A State Machine draws a message from its event pool, which is typically implemented as an event queue, and reacts to this message by firing one of its enabled transitions or by discarding it when no transition is enabled. This communication scheme is obtained for a ∆-Composite Structure structure C over EDHMLO by constructing an overall EDHMLO-structure over an EDHMLO-signature that reflects the parts, the ports, and the connections in its events and attributes, but includes explicit event queues as additional attributes. The overall EDHMLO-structure over this queue-based EDHMLOsignature then implements the selection of an event from a part's event queue, the reactions of this part to this event, and the distribution of the produced messages to the connected parts.

Formally, we construct a functor Sig q : Sig cs(EDHMLO) → Sig EDHMLO assigning to a Composite Structure signature ∆ the queue-based event/data signature Sig q (∆) = c∈Cmp(∆) (Sig(∆, c) ∪ {q c : Î(Sig(∆, c)) * }) and to a Composite Structure signature morphism the canonically cor- responding event/data signature morphism. For a Composite Structure signature ∆ and a part c ∈ Cmp(∆) there is a natural signature embedding η q ∆,c : Sig(∆, c) → Sig q (∆). For a ∆-Composite Structure structure C we construct an overall Sig q (∆)-event/data structure M C as follows: An overall configuration of M C consists, for each part c ∈ Cmp(∆), of an event queue q(c) ∈ Î(Sig(∆, c)) * stored in the attribute q c and a part configuration γ(c) ∈ Γ(C (c)); initially, all parts are in some of their initial configurations and all event queues are empty. The family of component control states forms the overal control state. In an overall configuration (q(c), γ(c)) c∈Cmp(∆) an overall transition to another overall configuration (q ′ (c), γ ′ (c)) c∈Cmp(∆) reacts to some î ∈ Î(Sig q (∆)) and outputs some Ô ∈ Ô(Sig q (∆)) * . This î can either instantiate some input event i ∈ I(Sig(∆, p * )) of some of the open ports p * ∈ Prt(∆) with c * = cmp(∆)(p), or it is the head of the event queue of some c * ∈ Cmp(∆) such that i ∈ I(Sig(∆, c * )). In the latter case, î is removed from the event queue of c * . In both cases, the reaction of part c * is any transition (γ(c * ), γ ′ * ) ∈ R(C (c)) î, Ô and overall γ ′ = γ{c * → γ ′ * }. Finally, all outputs p. ô ∈ Ô such that (p, p ′ ) ∈ Con(∆) and cmp(∆)(p ′ ) = c ′ are appended to the respective event queue of part c ′ , while preserving their order. This defines a natural transformation Mod cs(EDHMLO) q : Mod cs(EDHMLO) → Mod EDHMLO • Sig q with Mod

⟨|η(i) : F D A(η),X(i) (ϕ) ∧ (hd(q c ) = I(η)(i) ∨ open ∆,c (I(η)(i))) O(η)(O) : F 2D A(η),X(i)∪X(O) (ψ) ∧ a∈A(Sig q (∆))\(A(Sig(∆,c))∪{q c |c∈Cmp(∆)}) a = a ′ ∧ dist ∆,c (I(η)(i), O(η)(O), (q c , q ′ c ) c∈Cmp(∆) )|⟩Sen EDHMLO (η)(ϱ) ,
where hd yields the head of a queue, open checks whether the part's port for the event is open, the frame condition a = a ′ ranges over all attributes not pertaining to c or the queues, dist removes the input and distributes the outputs to the queues. Binding of control states remains unchanged.

For control state assertions s in a component d, it is necessary to remember that an overall control state is a family (member of a cartesian product) of the component control states. Therefore, in a Composite Structure, s has to be expressed by the data sentence s d = c(γ(d)), asserting that the component control state projected from s and that projected from the current component configuration are equal.

Satisfaction Relation and Satisfaction Condition

The satisfaction relation is an extension of that of EDHMLO: C |= cs(EDHMLO) ∆ ϱ if, and only if, Mod cs(EDHMLO) q,∆ (C ) |= EDHMLO Sig q (∆) ϱ.

Theorem 11.3 (Sig cs(EDHMLO) , Mod cs(EDHMLO) , Sen cs(EDHMLO) , |= cs(EDHMLO) ) is an institution.

Proof. This directly carries over from EDHMLO, as cs(EDHMLO)inherits everything except signatures directly from EDHMLO. However, we will unfold the definitions explicitly:

C ′ |σ |= cs(EDHMLO) ∆ ϱ ⇔ { def. |= cs(EDHMLO) } Mod cs(EDHMLO) q,∆ (C ′ |σ) |= EDHMLO Σ ϱ ⇔ { def. Mod cs(EDHMLO) q } Mod cs(EDHMLO) q,∆ (C ′ )|σ |= EDHMLO Σ ϱ ⇔ { satisfaction condition of EDHMLO } Mod cs(EDHMLO) q,∆ (C ′ ) |= EDHMLO Σ ϱ ⇔ { def. Sig q } C ′ |= cs(EDHMLO) ∆ ′ Sig q (σ)(ϱ) ⇔ { def. sentence translation } C ′ |= cs(EDHMLO) ∆ ′ σ(ϱ) 130

Satisfaction Relation and Satisfaction Condition

Corollary 11. 4 The comorphism to Casl also directly carries over from EDHMLO to cs(EDHMLO) by prefixing each of its components with Sig q .

Implementation of the UMLState Syntax in HeTS

To give the reader an idea of both the size of the system into which we integrated our work and the code itself which we wrote in that context, we report some line counts: The Haskell source files of HeTS after our changes have 284976 lines of code, including everything (comments, empty lines, etc.). Of these 1005 lines are in the files specifically dedicated to UMLState and its translation to Casl, 1285 lines are in the files dedicated to UMLStateO and its translation (adapted from the ones for UMLState) and 738 lines for UMLComp and its translation. We made minor changes to other parts of the HeTS codebase to enable HeTS to use our code. Moreover, we use the declarative nix package management language to reproducibly install dependencies. Our nix files contain a total of 280 lines.

Implementation of the UMLState Syntax in HeTS

A syntax in HeTS is implemented as an instance of the Syntax typeclass by giving a parser for basic specifications and a pretty printer, the latter being undefined in our case.

instance Syntax UMLState BASIC_SPEC Token () () where parsersAndPrinters UMLState = makeDefault (basicSpec [], pretty)

We define the abstract syntax in a style similar to a dedicated language for grammars. To be precise, for each non-terminal symbol we define an algebraic datatype for its syntax trees, e. That is, a BASIC_SPEC is given by a list of BASIC_ITEMS, which can be either SIG_ITEMS, VAR_ITEMS, SEN_ITEMS or EVENT_ITEMS. The deriving clauses add automatically derivable instances for some Haskell typeclasses. Here, they give us support for deciding equality and order among elements, for showing elements as strings and for a certain kind of generic programming.

Then we define a Parsec parser for each non-terminal, e.g.: The specification is handwritten in our language UMLState, which we crafted to resemble PlantUML. It has not been generated from a graphical notation, rather, the philosophy here would be to generate the graphical notation from the textual one. That said, it could be possible in the future to implement a (necessarily partial) translation from the XML-based XMI interchange format for UML.

In general, we algebraically build up the parsers from combinators (cf. Sect. 4.4). This approach to parsing allows us again to closely follow the structure of the grammar, while of course adding some operational details.

Implementing Static Analysis for UMLState

After parsing, we perform static analysis. Again, we give our implementation by instantiating a typeclass provided by HeTS:

Implementing Static Analysis for UMLState

The above is an implementation of the basic_analysis method of the StaticAnalysis typeclass of HeTS. At the core of this is the stateful action ana_BASIC_SPEC spec, where spec is the parse tree of a basic specification. The Haskell library function runStateT takes such a stateful action together with an initial state (here: mempty, i.e., the empty signature) and returns a pair of the action's return value and final state. The remainder of the above code is concerned with computing a symbol set for our signature and an (empty) list of annotations, as the method's return type requires. The goal of our static analysis is to report scoping errors (see, e.g., Fig. 12.3) and to extract signature items from the basic specification. The signature, which is the state and result of the static analysis, is of the following type1. -The event/data signature is realised as a map/dictionary data structure indexed by EVENT_NAMEs and Arities, the number of arguments. The names of the argument variables are not considered part of their identity -where two EVENT_NAMEs match except for the argument names, one of them will be dropped.

-Instead of one initial control state and initial state predicate, the formula contains a list of pairs of such. The reason is that Casl requires us to be able to combine two signatures by a monoidal operation. Changing to a list here seemed the best way to fulfil that requirement.

Like in the case of parsing, we can largely just follow the structure of the grammar, with state and errors being passed along implicitly using a monad: ana_BASIC_ITEMS :: BASIC_ITEMS -> Check BASIC_ITEMS ana_BASIC_ITEMS (SigB items) = SigB <$> ana_SIG_ITEMS items ana_BASIC_ITEMS (SenB items) = SenB <$> ana_SEN_ITEMS items ana_BASIC_ITEMS (EvtB items) = EvtB <$> ana_EVENT_ITEMS items ana_BASIC_ITEMS (VarB items) = VarB <$> ana_VAR_ITEMS items Mainly in the leaves of the syntax tree do we need to explicitly access the state, for both correctness checks and to compute the resulting library. E.g., the following code analyses an attribute declaration by first retrieving the state (the library computed so far), raising an error if an attribute with the same name has already been declared and finally, if there is no error, saving a new state with the variable added.

Translation of State Machines

Our translation algorithm into EDHML can be written in Haskell on a similar level of abstraction as it would be in pseudocode, due to the availability of list comprehensions and defined operators, including infix operators. As an example, we show the definition of EDHML sentences as an inductive data type and the expression for constructing the fin sentences. The latter corresponds to the fin family in line 13 and 14 of Alg. 1). Note, however, that the fin in the implementation takes the conjunction of the fins over all control states c, and explicitly takes arguments that were taken from the surrounding context in Alg. 1. Moreover, in the below we make use of a function complements that generates a list of the complemented pairs of sets used in Alg. 1. The plural variable names here (bs, es) correspond to the upper case variables there. The translation we register with HeTS goes directly from UMLState to Casl. We generate Casl signatures from the result of our static analysis. We have implemented a translation from EDHML to Casl sentences, which we apply to the EDHML sentence generated by our usual algorithm. As explained in Sect. 13.1, we have implemented some modifications to the formal comorphism that make proofs easier, such as Skolemisation and eliminating double negations. Moreover, as we have to generate basic rather than structured specifications, we leave imports from the standard library up to the user. For an example, see the specification in the appendices, i.e., App. C for the Counter machine and App. D for the ATM system. This also allows limiting the axioms that are brought into scope, which is often necessary for feasible fully automatic proving.

We then use these parts to define an instance of the Comorphism typeclass, just as we did before with the Syntax typeclass.

Design of Composite Structures and State Machines with Output

Our implementation of UMLStateO is similar to that of UMLState, with the main difference that we have to thread outputs through everything. To allow easier proofs and interoperability with UMLComp and other formalisms, we have further made the following design choices:

We now introduce a notion of port names and of messages. However, we wish to keep treating messages just like plain events as far as possible. In the input language, a message, consisting of a port name and an event name, is always treated as one unit. In the translation to CASL, we need separate types for events and messages, however, to enable the combination of State Machines with Composite Structures: Composite Structures consider events to be an opaque type, defined by State Machines, but they need to be able to change a message's sending port to its receiving port before inserting the message into the receiver's queue.

We further introduce a name for each machine specification (considered the machine type name), which we have to pass into most computations, because we include it in the names of the transition predicate, as well as most predicates and sorts. However, we have decided to not include the name in the event and message sorts and their operations, with the effect that those signature elements are shared between all State Machines and Composite Structures unless they are explicitly renamed. This removes the need of applying and reasoning about type conversions when a message is produced by one machine and consumed by another. We likewise give a name to a composite structure and to each of its components (machine instances).

Given these names, we generate a configuration sort, an initialisation predicate and a transition predicate, respectively, for each State Machine and the Composite Structure. These are identified using Casl's "same name, same thing" principle: They are named by appending the machine or structure name to ConfOf, initOf, and transOf. Moreover, we define a predicate with name distOf prepended to the Composite Structure name, which relates a list of output events to message queues before and after distributing those events.

As in the semantics, the configurations of the Composite Structure are defined to consist of a configuration and a message queue for each machine. By handling message queues in the Composite Structure, we simplify the machine definitions and ease separate reasoning about the communication and the internal behaviour of components.

The Composite Structure is in its initial configuration iff all the machines are in their respective initial configurations and, in addition, the queues are empty.

The Composite Structure makes a transition iff :

-the machine to which the input message is addressed can make a transition for this trigger for the indicated configurations and outputs, -the configurations of the other machines remain unchanged, -events are added to the queues as the distOf predicate and the output list require, and -the trigger message belongs to an external port or is removed from the appropriate queue.

Note that this behaviour of Composite Structures directly corresponds to that specified in Chapter 11, with the State Machines factored out as described here.

Design of Composite Structures and State Machines with Output

Messages from or to the outside do not interact with queues at all. They appear in the transition relations, but are otherwise ignored by the Composite Structure. As the Composite Structure itself is given by the same interface as a State Machine, it can itself become part of other Composite Structures which would then handle its external communication.

Extending the UMLState grammar to UMLStateO

We introduce MESSAGE_NAMEs, each consisting of a PORT_NAME and an EVENT_NAME. These new MESSAGE_NAMEs are used wherever we were using EVENT_NAMEs so far. BASIC_ITEMS ::= sig-its ⟨SIG_ITEMS⟩ | var-its ⟨VAR_ITEMS⟩ | evt-its ⟨MESSAGE_ITEMS⟩ | sen-its ⟨SEN_ITEMS⟩ EVENT_ITEMS become MESSAGE_ITEMS and gain a direction, so that in addition to inputs we can now also handle outputs. This turns:

EVENT_ITEMS ::= evt-it ⟨EVENT_ITEM + ⟩ EVENT_ITEM ::= EVENT_NAME VAR_NAME + VAR_NAME into: MESSAGE_ITEMS ::= (input | output) ⟨MESSAGE_ITEM + ⟩ MESSAGE_ITEM ::= MESSAGE_NAME VAR_NAME + VAR_NAME
Triggers become optional as we are now handling completion events, although without giving them a special priority. So we turn: TRANS_LABEL ::= TRIGGER ⟨GUARD⟩ ⟨ACTIONS⟩ TRIGGER ::= EVENT_ITEM

Interfacing with UMLStateO and UMLComp

The design we have described makes it possible to interface between UMLStateO, UMLComp and other formalisms. The recommended way to do so is by translating to Casl and combining the resulting specifications using Casl's structuring constructs. The best way to connect to UMLStateO is through UMLComp, or by the same interface used by UMLComp. UMLComp can connect with any formalisation that axiomatises compatible initialisation and transition predicates. In the following, we will show the sort, function and predicate symbols arising from the translation of a Composite Structure using our comorphism. For compatibility and maintainability, they can and should be imported from UMLComp.Logic_UMLComp. By excerpts from that module, we will now acquaint the reader with the interface our Composite Structures expose through the comorphism.

There are the following sort symbols, where each exists either once per machine type (not machine instance!) and once for the entire Composite Structure, or just once for the Composite Structure2. The below list contains each sort symbol paired with an (empty) set of supersorts. The list specifies a binary relation of sorts, the reflexive transitive closure of which will be Casl's subsorting relation for our specification.

--per machine type/composTy For an example specification that makes use of this interface for the case of UMLStateO and UMLComp, we refer the reader once more to App. D.

How to Obtain our Implementation

Our implementation is available as a fork3 of the HeTS git repository4. The current commit at the time of writing has the id dca77099c442c0df67111c54e5aa78f19d685609. We intend to contribute our work to upstream HeTS, but also to keep the version on which this thesis is based available in our fork. Within our fork, the file README.md contains information on how to build HeTS while recursively using the same versions of the dependencies that we also built with. In this chapter, we discuss two verification examples which we carried out using our methodology, formalisms and, to an extent, our newly developed tools. The material on the counter machine has been published in similar form as part of [START_REF] Rosenberger | Institution-based Encoding and Verification of Simple UML State Machines in CASL/SPASS[END_REF]. The material on the ATM scenario has been published as part of [START_REF] Rosenberger | An institutional approach to communicating UML State Machines[END_REF].

The examples and verification goals are the result of discussions with Alexander Knapp and Markus Roggenbach. The development of our general formalisms was in part guided by formalisations of the examples. I formalised the examples and carried out the proofs, including the development of necessary auxiliary lemmas, our trick for inductive verification without tool-support for the structured free construct, and the manual translation to KIV.

The ATM example is a variation on a popular theme; see, e.g., [START_REF] Knapp | Towards an Institutional Framework for Heterogeneous Formal Development in UML -A Position Paper[END_REF].

The Counter Machine: Proofs about State Machines without Outputs with HeTS and Spass

We implemented the translation of simple UML State Machines into Casl specifications within the heterogeneous toolset HeTS [START_REF] Mossakowski | The Heterogeneous Tool Set[END_REF]. Based on this translation we explain how to prove properties symbolically in the automated theorem prover Spass [WDF + 09] for our running example of a counter. Figure 13.1 shows the Casl specification representing the State Machine from Fig. 7.1, extended by a proof obligation %(Safe)% and proof infrastructure for it. We want to prove the safety property "cnt never exceeds 4" on the result of applying the comorphism, to make the specification more digestible to the theorem prover. These transformations include the removal of double negations, splitting a conjunction into separate axioms, and turning existentially quantified control states into constants by Skolemisation. Our automatic translation as implemented includes these transformations.

The ATM Scenario: Verifying Composite Structures with KIV

Recall the ATM example. For convenience, we repeat it's diagrams in Fig. 13.2 and briefly recall the scenario: An ATM and a Bank communicate to enable a user to withdraw money. This withdrawal should only be possible after the bank has confirmed that the user has entered the correct bank card and PIN.

We formalised1 , 2 the State Machines for the Bank and the ATM as well as their communication in Casl. We then set out to show the safety property: C(γ(atm)) = Verified → wasVerified(γ(bank)) = 1 This states that, whenever atm reaches the control state Verified, the bank's attribute wasVerified has the value 1. To recall some notation: γ(c) projects a component c's configuration from the system configuration; C projects the control state from a part's configuration; an attribute (here: wasVerified) gives us a projection from it's parts configuration.

We show the safety property by inductive verification, as justified by Prop. 10.3, using a stronger invariant. We first tried to show the preservation of said invariant using fully automatic provers connected to HeTS. Unfortunately, the handling of freely generated datatypes in this tool combination turned out not to be efficient enough without a laborious manual axiom selection that would defeat our goal of automation, leading us to employ the prover KIV.

KIV [EPS + 15] is an interactive theorem prover for program verification, which we used effectively as an automatic prover for first-order logic with freely generated types. There is currently no integration of KIV into HeTS, nor is there, to our knowledge, a formulation of its logic as an institution. However, for the fragment of KIV we are using we are confident that such a formalisation would be tedious, but straightforward. Consequently, we resorted to a manual translation to KIV, which we judged sufficient for demonstration purposes.

With our process clarified, we can define a KIV predicate for our safety property:

safe-def: safe(g) ↔ (ctrl(caConf(g)) = Verified → wasVerified(cbConf(g)) = 1); used for: s, ls;

The above introduces an axiom safe-def defining the predicate safe and marks the axiom for use as a simplifier rule (s) and a local simplifier rule (ls) for the KIV system. The predicate safe ranges over a type of system configurations, each consisting of the ATM configuration (caConf) and queue, as well as the bank configuration (cbConf) and queue. The machine configurations in turn consist of the control state and attributes. The safety predicate holds in a configuration iff, whenever ATM is in control state Verified, the Bank's attribute wasVerified has the value 1.

The behaviours of Bank and ATM are defined in the form of an initial state predicate and a transition predicate. For space reasons we show only one transition: The ATM transitions from one configuration to another, receiving an input event and sending out a list of messages. Each ATM configuration consists of (in that order) the control state, the card id to be verified, the PIN to be verified and the counter for the number of verification attempts. We give the definition of the transition predicate by a disjunction of the conditions of all syntactic transitions, including the control state before, the input event, the output list, variables to be set, the control state after and variables to remain unchanged. Given these machine predicates and a predicate dist to encode connectors, we can then define the transition predicate for the overall system: trans-def: trans(conf(ca1, qa1, cb1, qb1), in, out, conf(ca2, qa2, cb2, qb2)) ↔ dist(out, qa1, qa2, qb1, qb2) ∧ ( (atmTrans(ca1, in, out, ca2) ∧ cb2 = cb1 ) ∨ (bankTrans(cb1, in, out, cb2) ∧ ca2 = ca1)); used for: s, ls;

Initially, the queues are empty and the machines are in their initial configurations.

Having thus defined the machines, we turn to verification and define an invariant strong enough to show both its own preservation and our safety property. The essential idea is that we must control when the events allowing us to enter the Verified state on the ATM or to reset the wasVerified attribute of the bank are in the queues. Note that we can mostly ignore attribute values, as well as all distinctions between queue elements unrelated to our verification task. We can then formulate lemmas to the effect that this invariant does in fact imply the safety property, that it is satisfied in all legal initial configurations and that it is preserved by all transitions. These lemmas are as follows, again limited to one example for the transitions: Formulating separate lemmas for each transition instead of one lemma using the transition predicate helps us avoid a combinatorial explosion in the theorem prover.

Providing our specification to KIV with all definitions marked as simplifier rules and activating the heuristics mode "PL heuristics + structural induction", each of our lemmas is proved without noticeable delay, i.e., the verification of the invariant is successful and does not pose any difficulty to the prover.

At the moment, verifying other examples with this approach would proceed as follows:

1. formulate the system in UMLStateO and UMLComp

Summary

The UML was developed to unify existing modelling approaches and has successfully established itself as the main modelling language used in industry. It is the topic of ongoing research to establish formal semantics and tools for rigorous reasoning about UML models and the systems they specify. The work presented in this thesis forms part of one long-term effort [KMR15, KMRG15, KM17, Ros17] to develop such semantics and tools. Through it, we advance this effort significantly by providing concrete input languages and semantics for simple UML State Machines and Composite Structures. Further, we provide tool support for these UML models by implementing our languages in HeTS and providing well-behaved translations to Casl, which mediates access to existing general purpose provers, both interactive and fully automatic. We give exemplary models and properties involving typical challenges of inductive reasoning about software systems for which we show the feasibility of fully automatic verification. We approach the semantics of UML State Machines in two steps: Following a key insight we had in earlier work [START_REF] Rosenberger | Relating UML state machines and interactions in an institutional framework[END_REF], we first translate via a semantic function from a more direct State Machine description into a modal logic. This modal logic is built to require the presence or absence of sets of transitions in a way that admits the semantics-preserving translations of Institution Theory (i.e., signature morphisms and institution comorphisms). Once the semantic function has brought us into the realm of Institution Theory, we can then gain a semantically sound relationship with other formalisms by means of comorphisms.

We develop our State Machine language in two steps. The first only involves State Machines without output events, the second involves output events and adds ports in a somewhat transparent way. These extensions allow us to compose State Machines using an institution of Composite Structures, which we also introduce. Our two State Machine institutions and our Composite Structure institution are equipped with comorphisms to Casl, which can be composed with the numerous comorphisms out of Casl to other logics, allowing us to borrow [START_REF] Cerioli | May I borrow your logic? (transporting logical structures along maps)[END_REF] their proof systems and reasoning tools.

To sum up, our theoretical results are three new institutions for modelling sublanguages of the UML, each with a comorphism to Casl. Our practical contributions are -the development of concrete input languages for these institutions and a prototypical implementation for these languages and for our comorphisms in the Heterogeneous Toolset HeTS and -the verification, as a proof of concept, of two concrete example systems specified in UML, supported by our theory and tools.

Future Work

There are several immediate continuations of our work we can suggest. First, we suggest to create full automation for the generation of the auxiliary lemmas we needed to establish invariants in our examples. Next, it would be useful to link the data universe of EDHMLO to UML Class Diagrams (possibly following [START_REF] James | Designing Domain Specific Languages -A Craftsman's Approach for the Railway Domain Using CASL[END_REF]) and make types from the Class Diagrams available inside the implemented State Machines.

A larger project which would complete our automation, but also bring benefits beyond the world of UML, would be the addition of KIV to HeTS. In our practical verification attempts, KIV's direct support for inductive data types and for giving operational meanings to axioms or theorems made results feasible which were simply out of reach using HeTS's existing fully automatic provers. Not all the relevant constructs of KIV have direct correlates in Casl. In our experiments, our use of these inductive and operational KIV features was limited to defining a well-founded relation on the natural numbers and marking all axioms without distinction as rewrite rules. In general, good and fully automatic proof support might require one or more comorphisms using heuristics to recognise which of KIV's proof support constructs should be used where. Further, although there seems to be no reason to think KIV would not be an institution, to our knowledge this has never been formally established. To sum up, integrating KIV into HeTS would be a larger project, possibly a PhD project in itself, which could greatly improve HeTS's fully automatic capabilities for inductive reasoning, which is a central ingredient to the verification of models and programs.

Casting the net wider in the area of UML verification, it would be worthwhile to integrate UML Interaction Diagrams into HeTS and carry out experiments on how they can be related to State Machines and Composite Structures. Further, we suggest that there should be a systematic, experimental and theoretical study of notions of refinement between different UML models in HeTS and Institution Theory. The signature morphisms (for models of the same kind) and the comorphisms (between different kinds of models) would be the obvious starting points in the search for such notions.

Moreover, it would be worthwhile to connect to other formalisms for concurrent programming. Two such formalisms which are already available in the institutional world are the process algebra CSP and the (non-UML) State Machine based language Event-B. For CSP, an integration with CASL was developed in the form of CSP-CASL [START_REF] Roggenbach | CSP-CASL -a new integration of process algebra and algebraic specification[END_REF], an implementation of which 14.2. Future Work [Gim08, O'R12] has been integrated into upstream HeTS. Likewise, in the case of Event-B, there is a formalisation as an institution [START_REF] Farrell | Combining Event-B and CSP: An institution theoretic approach to interoperability[END_REF]. Event-B is a descendant of the successful B-method, which has been used, among other applications, to develop the verified control software for the driverless Paris metro lines [START_REF] Boulanger | Validation and verification of meteor safety software[END_REF]. The Event-B institution of [START_REF] Farrell | Combining Event-B and CSP: An institution theoretic approach to interoperability[END_REF] has also been implemented in a fork1 of HeTS. The fork features an integration of the Rodin tool for analysing Event-B models [START_REF] Farrell | Combining Event-B and CSP: An institution theoretic approach to interoperability[END_REF]. Unfortunately, it seems that this fork was never merged into upstream HeTS and has received no updates since 2015. It would be an opportunity for future work to integrate Event-B into upstream HeTS and perform a mixed case study involving, e.g., industry-supplied UML Composite Structure Diagrams and State Machines, a desired property expressed in CSP, and a development process by refinement in and code-generation from Event-B, all the while using HeTS to relate the different languages.

Finally, we would propose future work on the trustworthiness of HeTS itself. This is not only a moving target, as new logics get added to HeTS, but it is also a subtle challenge: A minimal trusted core in the tradition of LCF [START_REF] Milner | LCF: A way of doing proofs with a machine[END_REF][START_REF] Harrison | HOL light: A tutorial introduction[END_REF] can easily guarantee that a proof does in fact prove something. However, it is in general difficult to ensure that what has been proved is the intended property. In the case of a heterogeneous specification, this problem becomes even more difficult, as it involves the semantics of several languages and the translations between these. Making all of these part of a trusted core can hardly be acceptable. One way forward could be to create a high-trust code path connecting the proof rules on development graphs, as well as basic Casl specifications (or a subset thereof) to the core languages of one or a few provers. Trust in this code path could be established by a mixture of semantic modelling, formally proved theorems, and testing. Trust in other provers, where they output proof terms, can be replaced by reconstruction of their proof terms in one of the trusted core languages.

It would then be possible to model a system in a less trustworthy language of the HeTS ecosystem, and express the main theorems over this system in Casl (or its trusted subset), like we did in our verification examples. Auxiliary lemmas could then be phrased in any convenient language supported by HeTS. A lemma can then be translated into the language of a trusted prover, can be proved in that form, and used to prove the ultimately desired theorems. The correctness of the proof of a theorem would then depend on the formal correctness of the proofs of the translated lemmas within the trusted core, but not on the formal or intuitive correctness of the lemmas as originally phrased, or of their translation procedure into the core.

We are, of course, not the first to propose a verification of the logics and translations included in HeTS. In particular, the work we propose, in its formal aspects, will find a strong basis in the infrastructure and the logic atlas created by the LATIN project [CHK + 10].

Our main judgements are of the form Σ ⊢ w ▷ (∆, Ψ), meaning that over a signature Σ a word w is well-formed, and produces a signature extension ∆ and a set Φ of transition sentences (i.e., SEN_ITEMs). A signature is a triple of sets, the first containing states (STATE_ITEMs), the second attributes (VAR_ITEMs), the third events (the set is a function from name-arity pairs to EVENT_ITEMs). A signature extension is given by the same data. We make use of unions of signatures and signature extensions, which we define componentwise. We assume w to be a word over our abstract grammar. It is useful to think of these words as trees. in which each terminal symbol from the abstract grammar is an inner node and its parentheses enclose a subtree. This way, non-terminals whose defining rule involves no terminal symbol do not form sub-trees of their own and need not here be treated by their own semantic rules. Where there is no derivation tree to infer the well-formedness of a word in a given context, we consider it ill-formed, i.e., well-formedness is defined inductively.

We start with four rules which merely traverse subtrees and take the union of all the signature extensions and sentences produced. Earlier definitions are in scope for later ones. These rules are identical, except for the terminal symbol of the interpreted word.

Σ ∪ 0 i=1 ∆ i ⊢ it 1 ▷ (∆ 1 , Ψ 1 ) • • • Σ ∪ n-1 i=1 ∆ i ⊢ it n ▷ (∆ n , Ψ n ) Σ ⊢ basic-spec ⟨it 1 . . . it n ⟩ ▷ ( n i=1 ∆ i , n i=1 Ψ i ) Σ ∪ 0 i=1 ∆ i ⊢ it 1 ▷ (∆ 1 , Ψ 1 ) • • • Σ ∪ n-1 i=1 ∆ i ⊢ it n ▷ (∆ n , Ψ n ) Σ ⊢ var-its ⟨it 1 . . . it n ⟩ ▷ ( n i=1 ∆ i , n i=1 Ψ i ) Σ ∪ 0 i=1 ∆ i ⊢ it 1 ▷ (∆ 1 , Ψ 1 ) • • • Σ ∪ n-1 i=1 ∆ i ⊢ it n ▷ (∆ n , Ψ n ) Σ ⊢ sen-its ⟨it 1 . . . it n ⟩ ▷ ( n i=1 ∆ i , n i=1 Ψ i ) Σ ∪ 0 i=1 ∆ i ⊢ it 1 ▷ (∆ 1 , Ψ 1 ) • • • Σ ∪ n-1 i=1 ∆ i ⊢ it n ▷ (∆ n , Ψ n ) Σ ⊢ evt-its ⟨it 1 . . . it n ⟩ ▷ ( n i=1 ∆ i , n i=1 Ψ i )
An attribute can be added if it is not already in the signature. This produces a signature extension containing only the new attribute.

  are those from Sect. 2.1, but with an ASCII notation where ID is renamed to theid and n R to N_Reader, and the nonces, keys and ids are explicitly embedded into a common type of message data. Reaching s3 means a Tag has been verified. Reaching s4 indicates a failed verification. . . . . . . . . . . . . . . . . . . . . . . 2.3 Composite Structure Diagrams for our example protocol from Sect. 2.1. . . . . . . 2.4 PlantUML source for Fig. 2.2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.1 A possible accessibility relation for time over our weather signature. . . . . . . . . 3.2 A possible accessibility relation for places over our weather signature. . . . . . . . 3.3 A possible accessibility relation R(M)(nearby) over an extended weather signature. 4.1 A Casl specification for natural numbers. . . . . . . . . . . . . . . . . . . . . . . 4.2 The HeTS language graph, showing UMLState with the translation to Casl. Green as opposed to white indicates higher stability of the logic; blue indicates logics with direct prover support[MMCL14]. . . . . . . . . . . . . . . . . . . . . . . . . . . . 4.3 A development graph in HeTS. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4.4 The development graph from Fig. 4.3 after applying the global decomposition proof rule. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4.5 A context menu of actions possible on the red node from Fig. 4.4. . . . . . . . . . 4.6 The GUI for configuring proof attempts in HeTS. . . . . . . . . . . . . . . . . . . 4.7 A proof window in HeTS with some proof obligations resolved (in green) and some open. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4.8 A proof window in HeTS with some proof obligations resolved (in green), one timed out (in blue), and some open. . . . . . . . . . . . . . . . . . . . . . . . . . 5.1 A Class Diagram including an OCL constraint from [SWK + 10], specifying a processor with its registers. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.2 A diagram from [SWK + 10], showing the SAT-encoding of a system state which could be checked for conformance to Fig. 5.1. . . . . . . . . . . . . . . . . . . . . xv 5.3 A diagram from [SWK + 10], showing their verification flow. . . . . . . . . . . . . 5.4 Figure from [MSLF14],

  of how each movement in the mission of the train Green1 affects the train counters for critical sections A to Z, given in the form of a two-dimensional array. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.9 A Class Diagram from [KFdB + 05], showing the architecture of their example system, an implementation of the Sieve of Eratosthenes, a classical technique for generating prime numbers. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.10 A State Machine diagram from [KFdB + 05] for the Generator class from Fig. 5.9. 5.11 A State Machine diagram from [KFdB + 05] for the Sieve class from Fig. 5.9. . . . 5.12 A specification fragment in PVS from [KFdB + 05], showing the result of translating a transition of the Generator State Machine from Fig. 5.10, namely, the transition going from state_1 to state_1 and passing a number to the next Sieve. . . . . . 5.13 Two Class Diagrams from [Grö10] (given only textually) which, when combined, specify cyclical inheritance. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.14 A selection of language features from [Grö10]. . . . . . . . . . . . . . . . . . . . 5.15 Two Isabelle lemmas with proofs from [Grö10], the first stating that subclass relationships in a valid system model are non-circular, the second stating that they are transitive. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.16 The Isabelle theorem from [Grö10] establishing the incompatibility, in a particular language configuration, of the Class Diagrams from Fig. 5.13. Some proof steps about the unfolding of definitions have been skipped. . . . . . . . . . . . . . . . . 5.17 The Class Diagram for the calendar from [Grö10]. . . . . . . . . . . . . . . . . . . 5.18 The Object Diagram for the calendar from [Grö10]. . . . . . . . . . . . . . . . . . 5.19 The lemma from [Grö10] restating the invariant from the Class Diagram Fig. 5.17. 5.20 The lemma from [Grö10] restating the attribute values from the Object Diagram Fig. 5.18. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.21 The theorem from [Grö10] showing that the objects from Fig. 5.18 violate the constraint from Fig. 5.17. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.22 The State Diagram for the authentication system from [Grö10]. . . . . . . . . . . . 5.23 The Sequence Diagram from [Grö10] showing a hypothetical (illegal) run of the authentication system specified in Fig. 5.22. . . . . . . . . . . . . . . . . . . . . . Contributions and Publications . . . . . . . . . . . . . . . . . . . . . . . 3 1.2 Outline of the Remainder of this Thesis . . . . . . . . . . . . . . . . . . . 4

Figure 1

 1 Figure 1.1: UML diagrams for the ATM example verified in Sect. 13.2 (implicit completion events omitted): Composite Structure diagram: top; State Machines: left ATM, right Bank.

  Contents 2.1 Example: A Simple Security Protocol . . . . . . . . . . . . . . . . . . . . 8 2.2 Class Diagrams . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 2.3 State Machines . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 2.4 Composite Structure Diagrams . . . . . . . . . . . . . . . . . . . . . . . 11 2.5 Tools . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12

Figure 2

 2 Figure 2.1: A Class Diagram for the security protocol example.

Figure 2

 2 Figure 2.2: State Machine for the Reader from the security protocol. The conditions and actions are those from Sect. 2.1, but with an ASCII notation where ID is renamed to theid and n R to N_Reader, and the nonces, keys and ids are explicitly embedded into a common type of message data. Reaching s3 means a Tag has been verified. Reaching s4 indicates a failed verification.

  .3. The internal structure shown by a Composite Structure Diagram consists of a number of roles (drawn as boxes) with ports (little boxes on the borders of the roles) and connectors (shown by lines

  (a) A Reader by itself. (b) A Tag by itself. (c) A Reader and Tag put together. (d) An Intruder by itself. (e) A Reader, Tag and Intruder put together.

Figure 2

 2 Figure 2.3: Composite Structure Diagrams for our example protocol from Sect. 2.1.

  Figure 2.4: PlantUML source for Fig. 2.2

  Contents 3.1 Running Example: Modal Logics . . . . . . . . . . . . . . . . . . . . . . 15 3.2 Why use Institutions? . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17

3. 3

 3 Categories and Functors . . . . . . . . . . . . . . . . . . . . . . . . . . . 173.4 Institutions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 3.5 Example: An Institution for Modal Logics . . . . . . . . . . . . . . . . . 19 3.6 Comorphisms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24

Definition 3. 2

 2 A functor F between two categories C and D (written F : C → D, like for functions) is given by -an object part Obj(F) : Obj(C) → Obj(D), where we abbreviate Obj(F)(O) to F(O) -morphism parts, which are functions

Definition 3. 4

 4 An institution I is given by -a category Sig I , with objects called signatures, -a functor Sen I assigning -to each signature Σ a set Sen I (Σ) with elements called Σ-sentences and -to each signature morphism σ : Σ → Σ ′ a function Sen I (σ) : Sen I (Σ) → Sen I (Σ ′ ), -a functor Mod I from signatures to categories2 called "the reduct functor" assigning -to each signature Σ a category with objects called models and -to each signature morphism σ : Σ → Σ ′ a functor Mod I (σ) : Mod I (Σ ′ ) → Mod I (Σ) going backwards between the categories of models and -a relation |= I Σ ∈ Mod I (Σ) × Sen I (Σ) for each signature Σ, called the satisfaction relation fulfilling the satisfaction condition:

Figure 3 Figure 3

 33 Figure 3.1: A possible accessibility relation for time over our weather signature.

  Reduction for multimodal structures preserves the world set and transports accessibility relations and proposition satisfaction.

Definition 3 .

 3 19 A theory presentation T = (Σ, Φ) in the institution I consists of a signature Σ ∈ |Sig I |, also denoted by Sig(T), and a set of sentences Φ ⊆ Sen I (Σ). Its model class Mod I (T) is the class {M ∈ Mod I (Σ) | M |= I

Contents 4 . 1

 41 The Casl Language Family . . . . . . . . . . . . . . . . . . . . . . . . . 29 4.2 Heterogeneous Tooling with HeTS . . . . . . . . . . . . . . . . . . . . . 32 4.3 A Short Introduction to Haskell . . . . . . . . . . . . . . . . . . . . . . . 35 4.4 Parsec . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40

4. 1 .

 1 Figure 4.1: A Casl specification for natural numbers.

Figure 4

 4 Figure 4.2: The HeTS language graph, showing UMLState with the translation to Casl . Green as opposed to white indicates higher stability of the logic; blue indicates logics with direct prover support[MMCL14].

Figure 4

 4 Figure 4.3: A development graph in HeTS.Figure 4.4: The development graph from Fig. 4.3 after applying the global decomposition proof rule.

  Figure 4.3: A development graph in HeTS.Figure 4.4: The development graph from Fig. 4.3 after applying the global decomposition proof rule.

Figure 4

 4 Figure 4.5: A context menu of actions possible on the red node from Fig. 4.4.

Figure 4 . 6 :

 46 Figure 4.6: The GUI for configuring proof attempts in HeTS.

Figure 4

 4 Figure 4.7: A proof window in HeTS with some proof obligations resolved (in green) and some open.

Figure 4

 4 Figure 4.8: A proof window in HeTS with some proof obligations resolved (in green), one timed out (in blue), and some open.

[ 3 ]

 3 : instance Functor [] where fmap g [] = [] fmap g (x:xs) = g x : fmap g xs

[ 5 ]

 5 : incompleteHead (x:xs) = x [6]: incompleteHead [] <interactive>:1:1-25: Non-exhaustive patterns in function␣ →incompleteHead Another way of producing ⊥ is by explicitly raising an error: [7]: error "Oops..." Oops... CallStack (from HasCallStack):

  [8]: aList = [1,regress] anInfiniteList = [1,3..] sharingFun xs = incompleteHead xs + length xs Now the following computations all yield results:

  [14]: data EXPR = EXPR :+ TERM | EXPR :-TERM | TermExpr TERM deriving Show data TERM = TERM :* FACTOR | TERM :/ FACTOR | FacTerm FACTOR deriving Show data FACTOR = DigitFac DIGIT | ParensFac EXPR deriving Show type DIGIT = Char --['0'..'9']

  [15]: import Text.Parsec import Data.Functor ( ($>) ) type Parser t = Parsec String () t

  [20]: exprOpP :: Parser (EXPR -> TERM -> EXPR) exprOpP = do char '+' $> (:+) <|> do char '-' $> (:-) termOpP :: Parser (TERM -> FACTOR -> TERM) termOpP = do char '*' $> (:*) <|> do char '/' $> (:/) pairP :: Parser a -> Parser b -> Parser (a,b) pairP aP bP = do a <-aP b <-bP return (a,b) op

  [21]: factorP :: Parser FACTOR factorP = ( do DigitFac <$> digitP <|> do ParensFac <$> (char '(' *> exprP <* char ')') ) <?> "FACTOR" exprP :: Parser EXPR exprP = ( do term1 <-TermExpr <$> termP opsTerms <many $ pairP exprOpP termP return $ foldl op term1 opsTerms ) <?> "EXPR" termP :: Parser TERM termP = ( do fac1 <-FacTerm <$> factorP opsFacs <many $ pairP termOpP factorP return $ foldl op fac1 opsFacs ) <?> "TERM" parseTest factorP "7*5+8" DigitFac '7' [22]: parseTest factorP "(7*5+9)" ParensFac (TermExpr (FacTerm (DigitFac '7') :* DigitFac '5') :+␣ →FacTerm (DigitFac '9'))

  Verification of Finite UML Models . . . . . . . . . . . . . . . 44 5.2 Interactive Verification of Potentially Infinite Models . . . . . . . . . . . . 50

Figure 5

 5 Figure 5.1: A Class Diagram including an OCL constraint from [SWK + 10], specifying a processor with its registers.

Figure 5

 5 Figure 5.2: A diagram from [SWK + 10], showing the SAT-encoding of a system state which could be checked for conformance to Fig. 5.1.

Figure 5

 5 Figure 5.3: A diagram from [SWK + 10], showing their verification flow.

Figure 5

 5 Figure 5.4: Figure from [MSLF14], showing their tool-supported process for generating a model of an Automatic Train Supervision system.

Figure 5

 5 Figure 5.5: A metro network layout from [MSLF14].

  Fig. 5.7, defining what it means for all trains to have arrived, and then checking whether such a state is always finally reached, i.e., whether the CTL-like2 UMC formula holds. 2. There are forbidden transitions that would not necessarily lead to deadlocks (false positives). Such transitions can arise due to the way composite critical sections are identified. Eliminating the false positives requires refining the use of counters. No precise algorithm for this refinement is given, but examples of resulting UMC files are provided, and the process of finding false positives is outlined as follows: False positives are found by a) removing the conditions for entering critical sections from the model, but b) introducing an abstraction DEAD for the newly allowed states and c) establishing by model-checking that the formula holds, i.e., there is no reachable state that is marked as DEAD, but allows the eventual arrival of all trains.

Figure 5

 5 Figure 5.6: A state transition for the train Green1 from [MSLF14]. The array G1M is the train's mission. G1P is the train's position, given as an index into the mission. Missions from other trains are mentioned to forbid collisions.SA to SF are train counters for critical sections. The two-dimensional array G1C (an example defined in Fig.5.8 prescribes how movements of Green1 affect these counters. Each critical section counter also has a prescribed maximum value.

Figure 5

 5 Figure 5.8: A definition from [MSLF14] of how each movement in the mission of the train Green1 affects the train counters for critical sections A to Z, given in the form of a two-dimensional array.

Figure 5

 5 Figure 5.9: A Class Diagram from [KFdB + 05], showing the architecture of their example system, an implementation of the Sieve of Eratosthenes, a classical technique for generating prime numbers.

Figure 5 .

 5 Figure 5.10: A State Machine diagram from [KFdB + 05] for the Generator class from Fig. 5.9.

Figure 5 .

 5 Figure 5.11: A State Machine diagram from [KFdB + 05] for the Sieve class from Fig. 5.9.

Figure 5 .

 5 Figure 5.12: A specification fragment in PVS from [KFdB + 05], showing the result of translating a transition of the Generator State Machine from Fig. 5.10, namely, the transition going from state_1 to state_1 and passing a number to the next Sieve.

Figure 5 .

 5 Figure 5.13: Two Class Diagrams from [Grö10] (given only textually) which, when combined, specify cyclical inheritance.

Figure 5 .

 5 Figure 5.14: A selection of language features from [Grö10].

Figure 5 .

 5 Figure5.15: Two Isabelle lemmas with proofs from[START_REF] Grönniger | Systemmodell-basierte Definition objektbasierter Modellierungssprachen mit semantischen Variationspunkten[END_REF], the first stating that subclass relationships in a valid system model are non-circular, the second stating that they are transitive.

Figure 5 .

 5 Figure5.16: The Isabelle theorem from[START_REF] Grönniger | Systemmodell-basierte Definition objektbasierter Modellierungssprachen mit semantischen Variationspunkten[END_REF] establishing the incompatibility, in a particular language configuration, of the Class Diagrams from Fig.5.13. Some proof steps about the unfolding of definitions have been skipped.

Figure 5 . 17 :

 517 Figure 5.17: The Class Diagram for the calendar from [Grö10].

Figure 5 .

 5 Figure 5.18: The Object Diagram for the calendar from [Grö10].

Figure 5 .

 5 Figure 5.19: The lemma from [Grö10] restating the invariant from the Class Diagram Fig. 5.17.

Figure 5 .

 5 Figure 5.20: The lemma from [Grö10] restating the attribute values from the Object Diagram Fig. 5.18.

Figure 5 .

 5 Figure5.21: The theorem from[START_REF] Grönniger | Systemmodell-basierte Definition objektbasierter Modellierungssprachen mit semantischen Variationspunkten[END_REF] showing that the objects from Fig.5.18 violate the constraint from Fig.5.17.

Figure 5 .

 5 Figure 5.22: The State Diagram for the authentication system from [Grö10].

Figure 5 .

 5 Figure 5.23: The Sequence Diagram from [Grö10] showing a hypothetical (illegal) run of the authentication system specified in Fig. 5.22.

Figure 5 .

 5 Figure 5.24: A theorem from [Grö10] stating that the Sequence Diagram Fig. 5.22 violates the State Diagram Fig. 5.23.

Figure 5 .

 5 Figure 5.25: The Class Diagram and State Machine for the Bank example from [BBK + 04].

Figure 5 .

 5 Figure 5.26: A diagram from [BBK + 04] showing their verification flow.

Figure 6 . 1 :

 61 Figure 6.1: The languages and formalisms involved in our verification approach.

Figure 7

 7 Figure 7.1: Simple UML State Machine Counter

Figure 7 .

 7 Figure7.1 shows the example of a bounded, resettable counter working on an attribute cnt (assumed to take values in the natural numbers) that is initialised with 0. The counter can be reset to 0 or increased by a natural number k, subject to the current control state (s1 or s2) and the guards (shown in square brackets) and effects (after the slash) of the outgoing transitions. An effect describes how the data state before firing a transition (referred to by unprimed attribute names) relates to the data state after (primed names) in a single predicate; this generalises the more usual sequences of assignments such that cnt ′ = cnt + k corresponds to cnt := cnt + k and cnt ′ = cnt to a skip. The machine is specified non-deterministically: If event inc(k) occurs in state s1 such that the guard cnt + k = 4 holds, the machine can either stay in s1 or it can proceed to s2. Seemingly, the machine does not react to reset in s1 and to inc in s2. However, UML State Machines are meant to be input-enabled such that all event occurrences to which the machine shows no explicit reacting transition are silently discarded. We show the explicit transitions in red and the implicit ones in grey. Overall, the machine Counter shall ensure that cnt never exceeds 4: In fact, we will prove this in Chapter 13.For example (the reader can follow along in Fig.7.1), a run could -start in s1 with cnt = 0; then -consume inc(6), leaving us still in s1 with cnt = 0, as the limits cnt == 4 and cnt > 4 explicit, red transitions were exceeded; then -consume inc(3), leaving us still in s1, but now with cnt = 3; then -consume inc(1), taking us to s2 with cnt = 4; then -consume inc(2), leaving us still in s2 with cnt = 4 (via the grey self-loop on s2)

  and a ρ ∈ Sen EDHML (Σ) the satisfaction relation M |= EDHML Σ ρ holds if, and only if, M, ∅, γ 0 |= EDHML Σ,∅

  Definition . . . . . . . . . . . . . . . . . . . . . . . . . . . 89 8.2 Satisfaction Condition . . . . . . . . . . . . . . . . . . . . . . . . . . . . 93

Figure 8 . 1 :

 81 Figure 8.1: Frame for translating EDHML into Casl

Contents 9. 1

 1 The Underlying Data Universe . . . . . . . . . . . . . . . . . . . . . . . . 9.2 Data States and Transitions . . . . . . . . . . . . . . . . . . . . . . . . . 9.3 Events and Messages . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9.4 Event/Data Signatures . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9.5 Event/Data Structures . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9.6 Event/Data Formulae and Sentences . . . . . . . . . . . . . . . . . . . . . 9.7 Satisfaction Relation for EDHMLO . . . . . . . . . . . . . . . . . . . . . 9.8 Satisfaction Condition . . . . . . . . . . . . . . . . . . . . . . . . . . . .

Figure 9 . 1 :

 91 Figure 9.1: UML diagrams for the ATM example verified in Sect. 13.2 (implicit completion events omitted): Composite Structure diagram: top; State Machines: left ATM, right Bank.

  Fig. 4.1. The guards from Fig. 9.1 are examples of the open formulae. The formulae are open because they can contain both attributes and variables bound by the trigger specification. An example valuation {trialsNum → 2; cardId → 0; pin → 42} would not satisfy the formula trialsNum ≥ 3, whereas the valuation {trialsNum → 6; cardId → 0; pin → 2} would.

  input event signature morphism I(σ) : I(Σ) → I(Σ ′ ), an output event signature morphism O(σ) : O(Σ) → O(Σ ′ ), and a data signature morphism A(σ) : A(Σ) → A(Σ ′ ). We lift the event signatures and signature morphisms to messages by writing Î(Σ) for Ê(I(Σ)), Ô(Σ) for Ê(O(Σ)), Î(σ) for Ê(I(σ)), and Ô(σ) for Ê(O(σ)).

  For a Σ ∈ |Sig EDHMLO |, an M ∈ |Mod EDHMLO (Σ)|, and a ρ ∈ Sen EDHMLO (Σ) the satisfaction relation M |= EDHMLO Σ ρ holds if, and only if, M, ∅, γ 0 |= EDHMLO Σ,∅

  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 125 11.2 Structures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 127 11.3 Sentences . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 129 11.4 Satisfaction Relation and Satisfaction Condition . . . . . . . . . . . . . . 130

-

  a set Cmp(∆) of parts c, -each equipped with an EDHMLO-signature Sig(∆, c) for its input and output events and internal attributes; -a set Prt(∆) of ports p, each showing 125 11. UMLComp: Simple UML Composite Structures -an owning part cmp(∆)(p) ∈ Cmp(∆) as well as -an EDHMLO-signature Sig(∆, p) without attributes (i.e., A(Sig(∆, p)) = ∅) for its input and output events; and -a symmetric binary relation Con(∆) ⊆ Prt(∆) × Prt(∆) of connectors such that -for each part c ∈ Cmp(∆), the input and output events of Sig(∆, c) are the input and output events of c's ports prefixed with the port name, i.e., for F ∈ {I, O}, F(Sig(∆, c)) = p∈cmp(∆) -1 (c) {p. f | f ∈ F(Sig(∆, p))}; -for each part c ∈ Cmp(∆), the attributes of Sig(∆, c) are all prefixed with c, i.e., if a ∈ A(Sig(∆, c)), then a = c.a * ;

-

  a function Cmp(δ) : Cmp(∆) → Cmp(∆ ′ ) mapping parts, together with -an EDHMLO-signature morphism Sig(δ, c) : Sig(∆, c) → Sig(∆ ′ , Cmp(δ)(c)) for each c ∈ Cmp(Σ); -a function Prt(δ) : Prt(∆) → Prt(∆ ′ ) mapping ports, -together with an EDHMLO-signature morphism Prt(δ)(p) : Sig(∆, p) → Sig(∆ ′ , Prt(δ)(p)), preserving -the part c owning each port p, i.e., if c= cmp(∆)(p), then Cmp(δ)(c) = cmp(∆ ′ )(Prt(δ)(p)); -the connections, i.e., if (p, p ′ ) ∈ Con(∆), then (Prt(δ)(p), Prt(δ)(p ′ )) ∈ Con(∆ ′ ).The category of cs(EDHMLO)-signatures Sig cs(EDHMLO) consists of the Composite Structure signatures and signature morphisms over EDHMLO.Example 11.1 Considering the ATM example (Fig.9.1), we would have parts Cmp(∆) = {atm, bank}.

  Returning to the ATM example (Fig.9.1), let us now construct its queue-based signature 1. EDHMLO structures over this signature are then the Composite Structure structures for the ATM Composite Structure signature, here called ∆.locally formulated for this part can be faithfully transferred to the global Composite Structure, abbreviating the embedding η q ∆,c to η,

Figure 12

 12 Figure 12.1: The development graphs shown by HeTS after parsing the example files from Apps. C and D.

Figure 12 . 2 :

 122 Figure 12.2: Part of the output shown by HeTS for the resulting Casl specification System from App. D.

  g.: data BASIC_SPEC = Basic [BASIC_ITEMS] deriving (Eq,Ord,Show,D.Data) data BASIC_ITEMS = SigB SIG_ITEMS | VarB VAR_ITEMS | SenB SEN_ITEMS | EvtB EVENT_ITEMS deriving (Eq,Ord,Show,D.Data)

  Figure12.3: A brief excerpt from our Counter specification, together with a screenshot of the scoping error which results from removing line 3. The specification is handwritten in our language UMLState, which we crafted to resemble PlantUML. It has not been generated from a graphical notation, rather, the philosophy here would be to generate the graphical notation from the textual one. That said, it could be possible in the future to implement a (necessarily partial) translation from the XML-based XMI interchange format for UML.

instance

  StaticAnalysis UMLState BASIC_SPEC EDHML () () Library Morphism Token () where basic_analysis _ = Just $ \ (spec,sign,annos) -> do (spec',lib) <-runStateT (ana_BASIC_SPEC spec) mempty let sign = lib symSet = sign2SymSet $ lib2Sign lib extSign = ExtSign sign symSet annos = [] return (spec', extSign, annos)

  ana_VAR_ITEM :: VAR_NAME -> Check VAR_NAME ana_VAR_ITEM var = do lib <-get let vars = attrL lib when (var 'Set.member' vars) $ errC ("variable declared twice: " ++ show var) put $ lib { attrL = var 'Set.insert' vars } return var

  MESSAGE_NAME ::= PORT_NAME EVENT_NAME PORT_NAME ::= Token To the BASIC_SPEC we add a MACHINE_NAME to identify a machine in the context of a Composite Structure, so BASIC_SPEC ::= basic-spec ⟨BASIC_ITEMS + ⟩ becomes: MACHINE_NAME ::= Token BASIC_SPEC ::= MACHINE_NAME ⟨BASIC_ITEMS + ⟩In BASIC_ITEMS, we now have MESSAGE_ITEMS instead of EVENT_ITEMS.

[]

  The following predicate symbols are generated, where, as with the sorts, each symbol exists either for the Composite Structure and each machine type or just once for the entire Composite Structure. The list pairs each predicate symbol with the (singleton) list of types to which it can belong.--per machine type/composTy [ (pname, Set.fromList [pty]) | tyName <-composTy : machTys , (pname, pty) <-[ initP tyName , transP tyName ] ]

Figure 13

 13 Figure 13.2: UML diagrams for the ATM example verified in Sect. 13.2 (implicit completion events omitted): Composite Structure diagram: top; State Machines: left ATM, right Bank.

  atmTrans-def: atmTrans(atmConf(sa1, c1, p1, t1), in, out, atmConf(sa2, c2, p2, t2))↔ ∃ c : CardId, p : Pin . . . .∨ ( sa1 = CardEntered ∧ in = msg(userCom, PIN(p)) ∧ out = (msg(atmCompl, PINEnteredCompl) +l []) ∧ p2 = p ∧ sa2 = PINEntered ∧ c2 = c1 ∧ t2 = t1) ∨ .. .; used for: s, ls;

  invar-def: invar(conf(ca,qa,cb,qb)) ↔ ∃ x.(ctrl(ca) = Idle ∧ ctrl(cb) = Idle ∧ qa = empty ∧ qb = empty) ∨ (ctrl(ca) = CardEntered ∧ ctrl(cb) = Idle ∧ qa = empty ∧ qb = empty) ∨ (ctrl(ca) = PINEntered ∧ ctrl(cb) = Idle ∧ qa = enq(x, empty) ∧ qb = empty) ∨ (ctrl(ca) = Verifying ∧ ctrl(cb) = Idle ∧ qa = empty ∧ qb = enq(x, empty)) ∨ (ctrl(ca) = Verifying ∧ ctrl(cb) = Verifying ∧ qa = empty ∧ qb = enq(x, empty)) ∨ (ctrl(ca) = Verifying ∧ ctrl(cb) = VeriSuccess ∧ qa = empty ∧ qb = enq(x, empty) ∧ wasVerified(cb) = 1) ∨ (ctrl(ca) = Verifying ∧ ctrl(cb) = VeriFail ∧ qa = empty ∧ qb = enq(x,empty)) ∨ (ctrl(ca) = Verifying ∧ ctrl(cb) = Idle ∧ qa = enq(msg(bankCom, reenterPIN), empty) ∧ qb = empty) ∨ (ctrl(ca) = Verifying ∧ ctrl(cb) = Idle ∧ qa = enq(msg(bankCom, verified), empty) ∧ qb = empty ∧ wasVerified(cb) = 1) ∨ (ctrl(ca) = Verified∧ ctrl(cb) = Idle ∧ qa = enq(x, empty) ∧ qb = empty ∧ wasVerified(cb) = 1); used for: s, ls;

  lemmasSafe: invar(g) → safe(g); Init: init(g) → invar(g); . . .Trans6: g1 = conf(atmConf(Verifying, c, p, t), qa, cb, qb) ∧ qa ̸ = empty ∧ top(qa) = msg(atmCom, verified) ∧ g2 = conf(atmConf(Verified,c, p, t), enq(msg(atmCompl, VerifiedCompl), deq(qa)), cb, qb) ∧ invar(g1) → invar(g2);

  2. translate it (manually) into KIV 3. formulate the desired property 4. formulate the invariant and preservation lemmas 5. let KIV prove the lemmas We expect that further automation could remove the manual steps 2 and 4, leaving only 1. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 155 14.2 Future Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 156

  v ̸ ∈ Attr (State, Attr, Evt) ⊢ var-it ⟨v⟩ ▷ ((∅, {v}, ∅), Ψ) then %def %% Operations to represent natural numbers with digits: ops 1: Nat = suc(0); 2: Nat = suc(1); 3: Nat = suc(2); 4: Nat = suc(3); 5: Nat = suc(4); 6: Nat = suc(5); 7: Nat = suc(6); 8: Nat = suc(7); 9: Nat = suc(8); __@@__(m: Nat; n: Nat): Nat = m * suc(9) + n %(decimal_def)% then op __ + __ : Nat * Nat -> Nat, assoc, comm, unit 0; __ * __ : Nat * Nat -> Nat, assoc, comm, unit 1; forall r,s,t: Nat . (r + s) * t = r * t + s * t . t * (r + s) = t * r + t * s end spec GenerateSet [sort Elem] = %mono generated type Set[Elem] ::= {} | __+__ (Set[Elem];Elem) pred __eps__: Elem * Set[Elem] forall x,y: Elem; M,N: Set[Elem] . not x eps {} %(elemOf_empty_Set)% . x eps M+y <=> x=y \/ x eps M %(elemOf_NonEmpty_Set)% . M = N <=> (forall x: Elem . x eps M <=> x eps N) %(equality_Set)% end spec Set [sort Elem] given Nat = %mono GenerateSet [sort Elem] then %def preds isNonEmpty: Set[Elem]; __ isSubsetOf __: Set[Elem] * Set[Elem] ops {__}: Elem -> Set[Elem]; #__: Set[Elem] -> Nat; __ + __ : Elem * Set[Elem] -> Set[Elem]; __ -__ : Set[Elem] * Elem -> Set[Elem]; __ intersection __, __ union__,

where) = place Definition 3.9

  Modal sentences are defined by the grammar in Sect. 3.1.

	To recall, a sentence would be, e.g.:
	⟨place⟩ ((⟨time⟩ sunny) ∧ (⟨time⟩ raining))
	Definition 3.10 Moreover, given any signature Σ ∈ Obj(O), we define a category Mod(Σ) of
	all structures over Σ: An object M ∈ Obj(Mod(Σ)) is given by a Kripke frame, i.e.,
	-a set W(M), with elements called worlds,
	-relations R(M)(m) ⊆ W(M) × W(M) called (world) accessibility relations for all modality
	labels m ∈ M(Σ) and
	-a relation Sat(M) ⊆ W(M) × P(Σ) called proposition satisfaction.

  Mod : (Mod J • (ν Sig ) op ) → Mod I reducing models fulfilling the satisfaction condition M ′ |= Sen(ν)(ϕ) ⇐⇒ M ′ |ν |= ϕ.

	v)
	and ((M ′ |σ, v) |= ϕ))
	⇐⇒ [def. reduct ]
	(exists v ∈ W(M ′ |σ)
	s.t. R(M ′ |σ)(m)(w, v) and ((M ′ |σ, v) |= ϕ))
	⇐⇒ [def. sat. rel.]
	(M ′ |σ, w) |= ⟨m⟩ ϕ
	3.6 Comorphisms
	Definition 3.18 An (institution) comorphism [GR02] ν : I → J between institutions I and J
	is given by
	-a functor ν Sig : Sig I → Sig J translating signatures,
	-a natural transformation ν Sen : Sen I → (Sen J • ν Sig ) translating sentences and
	-a natural transformation ν

  Kyas et al. [KFdB + 05] introduce a translation of certain Class Diagrams, of non-hierarchical State Machines and of OCL constraints into the input language of the PVS theorem prover. Then they use PVS to interactively prove a safety property formulated in OCL. As intermediate steps, they formulate invariants directly in PVS and prove them.

  Chapter 7 explains EDHML, as well as why and how we embed State Machines into it. Appendix A contains the grammars (abstract and concrete syntax, static semantics) for our concrete State Machine input language UMLState. Chapter 8 introduces the theoroidal comorphism from EDHML to Casl.In a second step, we developed an extended notion of State Machines, suitable for combination in Composite Structures, on which we then built a notion of Composite Structures themselves. Our extended State Machine languages UMLStateO and EDHMLO are distinguished from the isolated versions mainly by the addition of output events and, in a mostly transparent way, of ports. We discuss these languages mathematically in Chapter 9 and the comorphism to Casl in Chapter 10. Chapter 11 outlines mathematically how an institution for Composite Structures can be built over EDHMLO. A comorphism to Casl is obtained with the help of a flattening into EDHMLO. In Chapter 12 we discuss our surface languages and their implementation in HeTS. Chapter 13 contains some verification experiments based on our approach.

	Chapter 7
	EDHML: An Institution for
	Embedding Simple State Machines

Contents 7.1 Example: The Counter Machine . . . . . . . . . . . . . . . . . . . . . . . 70 7.2 Event/Data Structures and the Problem with Institutionalising UML State Machines . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71 7.3 A Hybrid Modal Logic for Event/Data Systems . . . . . . . . . . . . . . . 76

In this chapter, we motivate and present an institution for the modal logic Event/Data Hybrid Modal Logic (EDHML), which allows us to embed Simple UML State Machines. As discussed in Chapter 3, modal logics are used to reason about notions of possibility and necessity. A hybrid modal logic additionally has constructs to require a sentence to hold in particular states/possible worlds. Events and data encode the notions of communication and state from UML which we wish to capture.

Chapter 13 Verification Examples Contents 13

  .1 The Counter Machine: Proofs about State Machines without Outputs with HeTS and Spass . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 147 13.2 The ATM Scenario: Verifying Composite Structures with KIV . . . . . . 149

To be precise, the sentences require a semantic transition to be possible if it conforms to some syntactic transition of the machine, and impossible otherwise.

Especially the handling of control states is surprisingly difficult.

We only formalise signals, not operations.

There is existing work on institutions for Class Diagrams, e.g.,[START_REF] James | Designing domain specific languages-a craftsman's approach for the railway domain using CASL[END_REF]. Connecting their work to ours could be a direction for future work.

https://en.wikipedia.org/wiki/List_of_Unified_Modeling_Language_tools

Proprietary software by Sparx Systems, available at: https://sparxsystems.com/products/ea/index. html

Free software (Eclipse Public License) available from: https://www.eclipse.org/downloads/packages/ release/2022-03/r/eclipse-modeling-tools

For a current list of PlantUML integrations, we refer the reader to https://plantuml.com/running

We will usually write composition omitting indices when types are clear. Where the category is clear, we will write morphisms as m : X → Y.

The reduct functor has the signature Mod I : (Sig I ) op → CAT. It comes from the opposite category of the category of signatures, i.e., the same category, except that morphisms go in the opposite direction. In other words, the functor Mod I reverses the direction of morphisms. For the target of this functor, some standard precautions have to be taken about size issues: It is the category of all (smaller) categories, which has to be large enough to include all categories of models we are interested in. This makes sense in any setting supporting a hierarchy of set universes.

What we call theoroidal institution comorphism was introduced as simple map of logics[START_REF] Meseguer | General logics[END_REF]. A similar notion using theories (closed under semantic consequence) instead of presentations (arbitrary sets of sentences) is called simple theroidal institution comorphism in[START_REF] Goguen | Institution morphisms[END_REF], where there is also a notion of theoroidal comorphism mapping from, as well as to, theories.

https://hets.eu/

In active development at https://github.com/spechub/Hets.

https://jupyter.org/

https://github.com/gibiansky/IHaskell

They are type level functions, which are also commonly called types in this context.

Some typeclass features, such as typeclasses with multiple parameters, require language extensions. Several such extensions are in common use.

This is the situation for Algebraic Data Types, "Int", "Char", etc., . For values of function types, λ-abstraction is treated somewhat like a constructor.

Hackage, the main Haskell package archive site, is accessible at https://hackage.haskell.org/.

Hackage reverse dependencies of parsec according to https://packdeps.haskellers.com/reverse/ parsec.

Hackage reverse dependencies of attoparsec according to https://packdeps.haskellers.com/reverse/ attoparsec.

An online interface to UMC can be accessed at http://fmt.isti.cnr.it/umc/V4.8/umc.html

CTL[START_REF] Clarke | Automatic verification of finite-state concurrent systems using temporal logic specifications[END_REF] (Computation Tree Logic) is an established branching-time temporal logic, of which UMC's UCTL is a variant.

In particular, this means that unlike us, they do not separate the ATM from the bank, because their focus is on the semantics of a single State Machine.

For more detail on these difficulties and their consequences for our approach, see Chapter 7.

We are traversing the graph spanned by the transition specifications, i.e., by the elements of T.

To recall from Sect. 7.2.2: A transition specification consists of an start control state c, a (data) state formula ϕ acting as a guard, an event e(X) acting as a trigger, a (data) transition formula ψ encoding the assignment actions, and resulting control state c ′ .

The translation indeed lands in Casl. However, as one of the referees pointed out, the structured free construct, which we use to define an inductive predicate, is not part of the Casl institution, but rather of Casl's institution independent structuring constructs. Structured specifactions over an arbitrary institution again form institutions, for many notions of structuring[START_REF] Durán | Structured theories and institutions[END_REF]. In particular, this is the case for freeness constraints[START_REF] Joseph | Institutions: Abstract model theory for specification and programming[END_REF] Def.

25, Prop. 26]. Our comorphism technically lands in such an institution over Casl.

We will omit some redundant information. Such omissions are indicated by dots (. . . ).

As a reminder, this sentence means: In the current configuration there are valuations and a transition for the incoming message and the outgoing messages such that these valuations satisfy the transition formula ψ and that ϱ holds afterwards.

In UMLState, we named this type Library, which is unfortunate, as it does not correspond to the library concept of Casl. In UMLStateO, the corresponding type is known as Sign. Moreover, in UMLState we have a Sign type which only contains those entries of Library that define symbols, i.e., not the initialisation and transition "sentences". Note however, that these are not proper sentences, as their effect is not limited to the exclusion of models. They do belong in the signature, and in UMLStateO we abolish the distinction.

Without renaming, they are even global, i.e., shared between Composite Structures.

https://github.com/rosento/Hets/

https://github.com/spechub/Hets/

The full formalisation of the ATM example, including an importable KIV project, is available in the digital appendix to[START_REF] Rosenberger | An institutional approach to communicating UML State Machines[END_REF] at https://rosento.github.io/2021-paper-composite/.

A heterogeneous formalisation of the ATM example using our languages UMLState and UMLComp can be found in App. D. However, this was not directly used for automatic verification for the reasons outlined in this section.

The Event-B fork of HeTS is available at https://github.com/mariefarrell/Hets.

Acknowledgements

PlantUML is primarily a graphical tool, not a semantic one, and it is easily possible to generate invalid diagrams. There is, however, experimental support for exporting models in XMI.

Building on the translation of formulae, the sentence translation ν Sen Σ : Sen EDHML (Σ) → Sen Casl (ν Sig (Σ))

only has to require additionally that evaluation starts in an initial state, as sentences are stated from the perspective of an initial state. Thus, sentence translation is defined by: -ν Sen Σ (ρ) = ∀g : Conf . init(g) ⇒ ν F Σ,∅,g (ρ)

Satisfaction Condition

The translation of Casl-models of Trans Σ into EDHML-structures and the translation of EDHML-formulae into Casl-formulae over Trans Σ fulfil the requirements of the "open" satisfaction condition of theoroidal comorphisms:

, an M ′ ∈ Mod Casl (ν Sig (Σ)), a v : S → C(ν Mod Σ (M ′ )), and a

.

Proof. We apply induction on the structure of Σ-event/data formulae.

Case φ:

Case s:

Case ↓s . ϱ:

Case (@ F s)ϱ:

Case ⟨e(X) ψ⟩ϱ:

Case ⟨|e(X) : ϕ ψ|⟩ϱ:

and some

and

Case ¬ϱ:

|, and ρ ∈ Sen EDHML (Σ). The satisfaction condition follows from

Events and Messages

An event signature E consists of a finite set of events |E| and a map s(E) : |E| → S(Dt) * assigning to each e ∈ |E| its list of parameter sorts. An event signature morphism η :

for all e ∈ |E|. We write e(X) for e ∈ |E| and s(E)(e) = s 1 , . . . , s n when choosing n different parameters X = x 1 , . . . , x n , and also e(X) ∈ E in this case; when f = e(X), we write X( f ) for X and we furthermore lift this notation to sets and lists of events. We sometimes identify the parameter list X with the S(Dt)-sorted family ({x i | s i = s}) s∈S(Dt) and write s(E)(e)(x i ) for s i .

A message e(β) over an event signature E is given by an event e(X) ∈ E with its parameters X instantiated by a parameter valuation β : X → D such that β(x) ∈ s D for s(E)(e)(x) = s; the set of all messages over an event signature E is denoted by Ê(E). When ê = e(β) ∈ Ê(E), we write β( ê) for β, and when e(X) ∈ E and β : Y → D for X ⊆ Y, we write e(β) for e(β↾X); both notations are furthermore lifted to sets and lists of messages.

Example 9.3 An event signature for the output events of the ATM machine in Fig. 9.1 could be given by: |E| = {bankCom.verify, userCom.ejectCard, userCom.keepCard} s(E)(bankCom.verify) = (Nat, Nat) s(E)(userCom.ejectCard) = () s(E)(userCom.keepCard) = () Note that these events contain port names (before the dot) in a way that is transparent to the formalism. This will be become important when we discuss Composite Structures. In our example signature, we have one event which takes two parameters of sort Nat and two events which take none. A message could then be given by (bankCom.verify, (7, 1)), which we write more conveniently as bankCom.verify(7, 1).

In order to mimic the UML 'ignore operator', we define the set of shuffling F1 ∥ F2 of two message lists F1 and F2 inductively by

An event signature morphism η : E → E ′ is lifted to a message e(β) ∈ Ê(E) by setting Ê(η)(e(β)) = η(e)(β) ∈ Ê(E ′ ) and also to sets and lists of messages.

Event/Data Signatures

An event/data signature Σ consists of input and output event signatures I(Σ) and O(Σ), and a data signature A(Σ). An event/data signature morphism σ : Σ → Σ ′ consists of an In this chapter, we define a (theoroidal) comorphism from EDHMLO to Casl, extending the comorphism from EDHML. The construction mainly follows the standard translation of modal logics to first-order logic [START_REF] Goranko | Modal logic[END_REF] and extends the scheme of Chapter 8 by outputs.

The contents of this chapter have been published in similar form as part of [START_REF] Rosenberger | An institutional approach to communicating UML State Machines[END_REF].

The construction of the comorphism was a common effort between Alexander Knapp, Markus Roggenbach and myself. In our virtual meetings, we jointly sketched the constructions, proofs and examples, which I then worked out in detail and wrote down in their final form.

Translating Signatures

The basis is a representation of EDHMLO-signatures and the frame given by EDHMLOstructures as a Casl-specification as shown in Fig. 10.1. The signature translation ν Sig : Sig EDHMLO → Pres Casl maps an EDHMLO-signature Σ to the Casl-theory presentation given by Trans Σ and an EDHMLO-signature morphism to the corresponding theory presentation morphism. Trans Σ first of all covers the events according to I(Σ) and O(Σ) with types InEvt and OutEvt, and the configurations with type Conf showing a single constructor conf for the control state from Ctrl and a data state given by assignments to the attributes from A(Σ). Furthermore, Trans Σ sets the frame for describing reachable transition systems with a set of initial configurations, a transition relation, and reachability predicates, where the specification of reachable uses Casl's "structured free" construct to ensure reachability to be inductively defined. Finally, a predicate mixed is included for representing the shufflings of a list of outputs with some additional output events.

Reducing Structures

The model translation

then can rely on this encoding. In particular, for a model

for the configurations as well as

The EDHMLO-structure resulting from a Casl-model M ′ of Trans Σ can thus be defined by

Translating Sentences

For EDHMLO-sentences, we first define a formula translation

which, mimicking the standard translation, takes a variable g : Conf as a parameter that records the "current configuration" and also uses a set S of state names for the control states. The translation embeds the data state and 2-data state formulae using the substitution

for replacing the attributes a ∈ A(Σ) by the accessors a(g). The translation of EDHMLO-formulae then reads

Building on the translation of formulae, the sentence translation

only has to require additionally that evaluation starts in an initial state:

-

Proof. We proceed by structural induction over ϱ. Case φ:

Case s:

Case ↓s . ϱ:

Case (@ J,N s)ϱ:

and

Case ¬ϱ:

Theorem 10.2 (ν Sig , ν Mod , ν Sen ) is a theoroidal comorphism from EDHMLO to Casl.

Proof. Let Σ ∈ Sig EDHMLO , M ′ ∈ |Mod Casl (ν Sig (Σ))|, and ρ ∈ Sen EDHMLO (Σ). The satisfaction condition follows from

For a Casl-proof of an EDHMLO-invariant 2φ such that φ has to hold in every reachable configuration, the full generality of the reachable predicate can sometimes be avoided by replacing the proof obligation ∀g : Conf . reachable(g) ⇒ F Casl ν Sig (Σ),A(Σ)(g) (φ) by the usual stepwise induction scheme that only requires to demonstrate the invariant to hold in all initial configurations and that it is preserved by every transition. Moreover, the EDHMLO-state formula φ can be generalised into a Casl-invariant.

Proposition 10.3 Let (Σ, P) be a theory presentation in EDHMLO and (ν Sig (Σ), Φ) a theory presentation in Casl such that Mod Casl (ν Pres (Σ, P)) ⊆ Mod Casl (ν Sig (Σ), Φ). Let inv Casl (g) ∈ F Casl ν Sig (Σ),{g} be a Casl-formula with a single free variable g and inv EDHMLO ∈ F D A(Σ),∅ an EDHMLO-state formula, such that

The ports of the ATM Composite Structure could be given as:

Prt(∆) = {atm.bankCom, atm.userCom, bank.atmCom}

The connectors could then be given by:

To all this, we could add a completion event for each control state of each part and a completion port, connected to itself, for each part.

Structures

For an cs(EDHMLO)-signature ∆, a ∆-Composite Structure structure (sic!) over EDHMLO is a family

consisting of an EDHMLO-structure for each part c. The δ-reduct C ′ |δ of a ∆ ′ -Composite Structure structure C ′ over EDHMLO along a Composite Structure signature morphism δ : ∆ →

Sentences

First, we have have input and output events with their sorts:

Then, we have the attributes, now crucially including the queues:

Like before, we could add completion events.

Sentences cs(EDHMLO) inherits the event/data formulae of EDHMLO:

Sen cs(EDHMLO) = Sen EDHMLO • Sig q and the underlying D, though extended by queue attributes. In particular, we have for a part c ∈ Cmp(∆) that a transition sentence2 In this chapter, we describe the implementations of our institutions and comorphisms in the Heterogeneous Toolset HeTS. To be precise, we implemented the languages UMLState (State Machines without outputs), UMLStateO (State Machines with outputs) and UMLComp (Composite Structures), and, for each of the above, a translation to Casl.

The concepts underlying these implementations are the result of joint work with our coauthors in [START_REF] Rosenberger | Institution-based Encoding and Verification of Simple UML State Machines in CASL/SPASS[END_REF][START_REF] Rosenberger | An institutional approach to communicating UML State Machines[END_REF]. The implementation itself and its description here are exclusively the work of the present author.

The precise UMLState input language we implement is specified in App. A. We have crafted it to resemble PlantUML. For UMLStateO, the changes to the input language are discussed in this chapter as part of a discussion of the design choices for our implementation. A heterogeneous specification involving UMLState is given in App. C, another one for an example system involving UMLStateO and UMLComp is given in App. D. In the case of UMLState, the specification is the one for our Counter example on which we actually perform our proofs in Chapter 13. In the case of UMLStateO and UMLComp, we show the ATM example. For this, we have performed proofs on a manual translation into KIV, for reasons we explain in Chapter 13. Figure 12.1 shows the development graphs resulting from parsing and analysing these two specifications. Part of the output of the automatic translation for the ATM example can be seen in Fig. 12.2. The reader may wish to take a moment to compare the two before we continue in the next section with an explanation how to interface with our languages. The following are the types and constructors for which the translation of a Composite Structure will contain the symbols and freeness axioms:

--Constructors for free types.

--Note that machine specific types, --as well as event types, --are not free as far as the composite structure is concerned. )

%% induction scheme for "reachable" predicate, instantiated for "invar":

. . machine axioms . . . then %implies %% the safety assertion for our counter:

%(Safe)% %% steering Spass with case distinction lemmas, could be generated algorithmically: using the automated theorem prover Spass.

The Casl specification Counter imports a specification Trans which instantiates the generic frame translating EDHML into Casl, cf. Fig. 8.1. However, the first-order theorem prover Spass does not support Casl's structured free construct that we use for expressing reachability. For invariance properties this deficiency can be circumvented by loosely specifying reachable (i.e., omitting the keyword free), introducing a predicate invar, and adding a first-order induction axiom. This means that we have to establish the safety property for a larger model class than we would have with freeness. When carrying out symbolic reasoning for invariants referring to a single configuration, the presented induction axiom suffices. Other properties would require more involved induction axioms, e.g., referring to several configurations.

Then the specification provides the machine axioms as stated (partially) in Thm. 7.13. The axioms following the %implies directive are treated as proof obligations. We first state the safety property that we wish to establish: in all reachable configurations, the counter value is less or equal 4 -%(Safe)%. The remainder steers the proving process in Spass by providing suitable case distinctions. For invariants referring to a single configuration, these could also be generated automatically based on the transition structure of the state machine, although we have written them by hand.

As a proof of concept, we automatically verified the safety property from Fig. 13.1 in Spass. In this experiment, we performed some optimising, semantics-preserving logical transformations

Part III

Conclusions

Appendix A

Language Definitions for UMLState

A.1 Lexical Primitives

The following lexical primitives are available. Their syntax is that of ordinary (non-mixfix) Casl identifiers or of (unsigned decimal integer) numerals.

VAR_NAME ::= Token EVENT_NAME ::= Token STATE ::= Token NAT_LIT ::= Int

A.2 Abstract Syntax

With these lexical primitives in place, we can now define the abstract syntax of UMLState. We stay close to the BNF-like notation usual in CASL-related work, our main departure being the explicit parentheses for rules including terminal symbols: terminal ⟨NONTERMINALS⟩ This choice emphasises the tree structure which the grammar induces on each word of the language, which simplifies our description of the static semantics.

Each rule of the abstract syntax expands a non-terminal symbol, written to the left of ::=. The expansion, written on the right may contain a leading terminal symbol, written in lower case. If a terminal symbol is present, the rest of the expansion is parenthesised as shown above. The remaining symbols are non-terminals, where the Kleene plus can be added to indicate the possibility of repetition. Both non-terminals and parts of terminals can be underlined to mark them as optional.

Given these conventions, the following grammar is then an abstract description of parse trees for UMLState basic specifications, which can be embedded in HeTS heterogeneous specifications. The terminal symbol at the root is BASIC_SPEC.

BASIC_SPEC ::= basic-spec ⟨BASIC_ITEMS + ⟩ A basic specification consists of a number of items, each of which introduces variables or events into the signature, or describes a (possibly initial) transition the machine should contain. The following terms, actions and data formulae are available in UMLState as we implemented it. Note that these are specific to the natural numbers as our data universe, whereas our institution as formalised is parametric in the data universe used. Data formulae are a subset of Casl.

TERM

A.3 Concrete Syntax

The grammar for the concrete syntax follows conventions similar to those for the abstract syntax. We make the connection between the two grammars by using the same non-terminal symbols. Terminal symbols can now be anything that is not a non-terminal or meta-symbol, and are freely mixed with the non-terminals. Repetition now indicates a separator to be used (comma or semicolon) and is given in the form NON_TERM; . . . ; NON_TERM or NON_TERM, . . . , NON_TERM.

As in the case of the abstract syntax, we start with the rules for basic specifications and the various items they can consist of.

A.4 Static Semantics

With the abstract and concrete syntax in place, we can now turn to the description of the static semantics of UMLState, which we will describe in the style of natural semantics ( [START_REF] Gordon D Plotkin | A structural approach to operational semantics[END_REF][START_REF] Kahn | Natural semantics[END_REF]).

A state can be introduced if it is not already in the signature. The resulting signature extension contains only the new state.

s ̸ ∈ State (State, Attr, Evt) ⊢ st-it ⟨s⟩ ▷ (({s}, ∅, ∅), ∅)

A sentence for an initial transition can be introduced if the target states and all variables of the guard are in the signature. The sentence is given as an added sentence.

The definition of a new event is valid if no event with the same name and arity is already contained in the signature. The signature extension contains just a mapping from the name and arity of the new event to the word defining it.

(name, |vars|) ̸ ∈ dom(Evt) (State, Attr, Evt) ⊢ evt-it ⟨name vars⟩ ▷ ((∅, ∅, {(name, |vars|) → evt-it ⟨name vars⟩}, ∅) A transition item is valid if its source and target state are defined, the trigger is defined up to renaming of parameters and the guard and actions are valid. We define guard and action validity by separate judgement forms. Their definitions amount to saying that a guard is valid if all its variables are either defined attributes or trigger parameters, and an action is valid if it assigns a valid term to a known attribute. Term validity follows the same rule as guard validity. {s 1 , s 2 } ⊆ State (Attr, e) ⊢ g guard (Attr, Evt, e) ⊢ a actions (State, Attr, Evt) ⊢ trans-it ⟨s 1 s 2 e g a⟩ ▷ ((∅, ∅, ∅), {trans-it ⟨s 1 s 2 e g a⟩}) vars(g) ⊆ Attr ∪ evars (Attr, evt-it ⟨ename evars⟩) ⊢ g guard

Diagrams for the Security Protocol Example

Here we show the remaining diagrams for the State Machine example. Note that the nondeterministic choice expression used by the Dolev-Yao intruder is not directly representable in UMLState or UMLStateO. We can could, however, express it in Casl and still link to it via UMLComp.

The reader will here observe a downside of PlantUML, namely, that it is not good at laying out self-loops. %% induction scheme for "reachable" predicate, instantiated for invar forall es:EvtNameSet . ( forall g:Conf . init(g) => invar(g) ) /\ ( forall g,g':Conf; e:Evt . (reachable2(es,g) => invar(g)) /\ reachable2(es,g) /\ trans(g,e,g') => invar(g') ) => ( forall g:Conf . reachable2(es,g) => invar(g) ) %(InvarIsReachableInd)% then %implies %% case distinction lemmas, can be generated algorithmically forall g,g':Conf; e:Evt; k:Nat . init(g) => invar(g) %(InvarInit)% . (reachable2(allEvts,g) => invar(g)) /\ reachable2(allEvts,g) /\ trans(g,e,g') /\ e=evt_reset => invar(g') %(InvarReset)% . (reachable2(allEvts,g) => invar(g)) /\ reachable2(allEvts,g) /\ trans(g,e,g') /\ e=evt_inc(k) => invar(g') %(InvarInc)% . (reachable2(allEvts,g) => invar(g)) /\ reachable2(allEvts,g) /\ trans(g,e,g') /\ e=evt_inc(k) /\ ctrl(g)=s1 /\ cnt(g)+k<4 => invar(g') %(InvarInc)%

Appendix D

A Heterogeneous Specification for the ATM example