Abstract Automata learning is an approach for extracting a model in the shape of an automaton from a black-box system. This approach has recently gained much attention in both industry and academia. In this paper, we introduce a compositional automata learning algorithm for systems comprising synchronous parallel components. Our algorithm assumes no prior knowledge about the number of components, their individual alphabets, and the synchronizing alphabets. The learning process is automatic and figures out the alphabet symbols on-the-fly during learning the components. We prove that the proposed algorithm terminates and correctly learns the individual components. We use a number of case studies from the industrial automotive domain and synthetic benchmarks to evaluate the performance of the proposed algorithm. The experimental results show that the algorithm requires significantly fewer input symbols and resets to learn the system compositionally.

In the new generation of message-based systems such as network-based smart systems, distributed components collaborate via asynchronous message passing. In some cases, particular ordering among the messages may lead to violation of the desired properties such as data confidentiality. Due to the absence of a global clock and usage of off-the-shelf components, there is no control over the order of messages at design time. To make such systems safe, we propose a choreography-based runtime enforcement algorithm that given an automata-based specification of unwanted message sequences, prevents certain messages to be sent, and assures that the unwanted sequences are not formed. Our algorithm is fully decentralized in the sense that each component is equipped with a monitor, as opposed to having a centralized monitor. As there is no global clock in message-based systems, the order of messages cannot be determined exactly. In this way, the monitors behave conservatively in the sense that they prevent a message from being sent, even when the sequence may not be formed. We aim to minimize conservative prevention in our algorithm when the message sequence has not been formed. The efficiency and scalability of our algorithm are evaluated in terms of the communication overhead and the blocking duration through simulation.