Modularity for system modelling and analysis

The domain of this thesis is concurrency theory and formal models of distributed systems. In particular, we work in the fields of modularity and compositionality. We model the system structure by Petri Nets, in particular Elementary Net Systems, and system behaviour by Transition Systems or Occurrence Nets. We work with morphisms: a theoretical tool used to represent formal relations between models. The relation modelled can be a transformation, an abstraction, a refinement or other. Here, we focus on refinement/abstraction. One of the main challenges consists in developing languages and methods allowing to derive properties of the refined system from properties of the abstract system. Starting from some notions of morphisms already defined in the literature, we study the possibility of varying or restricting these definitions so to preserve and reflect structural and behavioural properties of the related systems. Our main contribution in this part is the definition of α-morphisms, which preserve reachable markings. Our approach is motivated by the attempt to define a refinement operation preserving behavioural properties on the basis of structural and only local behavioural constraints. Indeed, we characterize the local additional restrictions, with respect to general morphisms, that aim, on one hand, to capture typical features of refinements, and on the other hand to ensure that some behavioural properties of the abstract model still hold in the refined model, like the reflection of reachable markings and that α-morphisms induce a bisimulation between the related Net Systems. In order to define a structural morphism able to preserve and reflect behavioural properties, it is natural to search also a behavioural morphism that formalises this goal. As we already said, we consider both Occurrence Nets and Transition Systems to represent the behaviour of systems modelled by Elementary Net Systems. Clearly it is possible to see an Occurrence Net as an Elementary Net System, putting a token in each initial place of the Net. So, it is possible to use the morphisms already defined also on Occurrence Nets. We can use the concurrency, conflict and causality relations to obtain simpler morphisms on Occurrence Nets such that the same results obtained for Elementary Net Systems still hold. In dealing with morphisms on Elementary Transition Systems, our contribution is the definition of Γ-morphisms, that take into account also the relations between states and transitions. Moreover, we want to relate morphisms between Elementary Net Systems with morphisms between their associated behavioural models and vice versa, in order to obtain more behavioural properties relating only structural models. In the development of distributed systems a central role is played by formal tools supporting various aspects of modularity such as compositionality. There is a lot of interest in how to combine models because it makes the analysis of models simpler and more structured. The use of products in a suitable category of Nets as a way to model composition by synchronization has been studied by several authors. Following an approach already presented in literature, the basic idea consists in composing two different refinements of a common abstract view, obtaining a new model which describes the system comprising the details of both operands, while complying to the same abstract view. The rules for identifying elements of the components are expressed by means of morphisms towards another model, called interface. The interface can be seen as an abstraction of the whole system, shared by the components or, alternatively, it can be interpreted as the specification of the communication protocol. In this case, each operand can be seen as made of the actual, local, component, and of an interface to the rest of the system. The composed system is made by local parts corresponding to each component and a global part corresponding to the interaction between the components. The composed system results to be related to both the components and the interface by means of morphisms, and the resulting diagram is commutative. Our contribution is the adaptation of this procedure to α-morphisms, so that the results obtained for these morphisms can be used in composition. Using α-morphisms we are able to obtain a composed system that is bisimilar to one of the components, if the other component respects the behavioural constraint local to each refinement of the interface. How could a system designer use these results in practice? One way would consist in defining a set of Net transformations that he or she may use in refining a system model. Such transformations should be consistent with a suitable class of morphisms in the following sense: the result of applying a Net transformation should map onto the initial more abstract model. Our contribution consists on showing two examples of this kind of Net transformations. The theoretical framework constituted by the composition guided by morphisms and interface is suitable to be used in the field of information flows and visibility. In this part of the research we assume to have a system divided in a hidden part (called the high part or the defender) and an observable part (called the low part or the attacker). The observer knows the structure of the whole system, but he is able to observe only the observable part. The observer can see the state of a part of the system, and observing this, it is able to derive that one event has occurred. We want to understand if the observer is able to infer some information on the local states of the hidden part. We aim at a structural characterization of the hidden internal states of a system that become visible after its interaction with a defined subsystem. We assume to have a high-level system that wants to keep secret its internal local states from a low-level system interacting with the high-level component through an interface. The new part of our proposal is that we use the local validity of conditions as observable properties and we focus on structural properties. Our contribution here is in changing the point of view of the attacker: he is not able to observe events, but only the modification of the local states. Defining a new kind of observability on states, we obtain results on the visibility of conditions of the defender that the attacker is able to infer using invariant properties that concern conditions of the defender and of the interface. We also define a classification of systems related to the idea of visibility.