In this paper, we propose an approach that allows to limit the verification of an LTL property of a modular system to the parts that it concerns. Given a modular Petri net and a property that concerns one module, the model checking is performed by exploring exclusively an abstract graph that models the behaviors of the module and is enriched with some global information. Thanks to a distributed state space version, named Reduced Distributed State Space (RDSS), of the considered modular system, there is no need to explore graphs of irrelevant modules to the property. We used the SPOT library to implement the suggested model checking in a C++ prototype, and we compared our primary results with those of the LTSmin model checker.

Opacity is a security property that guarantees the confidentiality of secret information from a partial observer of the system. To address this problem, we propose a modular approach that uses Supervisory and Control Theory to design a global supervisor for Modular Discrete Event Systems (MDES). This approach assumes the attacker can observe the shared alphabet between modules, and takes into account the modular structure of the system; which significantly decreases computational complexity compared to monolithic methods. To achieve this, we introduce a reduced-complexity algorithm, based on the Hyper Symbolic Observation Graph. The HSOG is an abstraction graph that considers only events that have a direct impact on the opacity. This reduces the number of states to be considered, making the algorithm more efficient.

Discrete Event systems are dynamic systems with two main characteristics: their set of states is discrete and their dynamic is event driven (as opposed to time driven). In this paper, we study a security property for DES called opacity. A system$\mathcal{T}$, partially observed by a third party -called an attacker- is said to be opaque if the attacker can never conclude from its provided interface that$\mathcal{T}$is in a secret state. Given a critical system that may leak confidential information, an attacker and a subset of controllable actions, we propose an approach to synthesize a controller that enforces the system's opacity. This controller is designed as a function that applies, at run time, on the current executions to disable any controllable action that eventually leads to the violation of the system's opacity. Our approach is based on a novel graph called a Hyper Symbolic Observation Graph. The language obtained under control is proven to be maximal whatever is the relationship between the attacker and the controller observations.

This paper deals with the modular analysis of distributed concurrent systems modelled by Petri nets. The main analysis techniques of such systems suffer from the well-known problem of the combinatory explosion of state space. In order to cope with this problem, we use a modular representation of the state space instead of the ordinary one. The modular representation, namely modular state space, is much smaller than the ordinary state space. We propose to distribute the modular state space on every machine associated with one module. We enhance the modularity of the verification of some local properties of any module by limiting it to the exploration of local and some global information. Once the construction of the distributed state space is performed, there is no communication between modules during the verification.