Distributed systems have been widely used in various domains. However, the concurrent and asynchronous nature makes their safety and reliability hard to guarantee, especially in the design phase. In this paper, we extend Mediator and its semantics to capture the inherent real-time and asynchronous behavior in distributed systems. As a component-based language, Mediator provides a compositional modeling framework and corresponding precise formal semantics, making it able to reuse reliable components in different contexts.

Formal modeling and verification of component connectors in complex software systems are getting more interests with recent advancements and evolution in modern software techniques. Various properties of connectors can be specified as high-order logic propositions and verified using theorem proving techniques. However, most high-order logic provers still highly rely on human interactions and thus make the proving process difficult and time-consuming. In this paper, we propose an approach based on recurrent neural networks (RNNs) to predict the correct tactics in the proving process. Recurrent layers consisting of Long-Short-Term-Memory (LSTM) units provide a better correctness rate comparing with simple RNN units. Under this framework, properties of connectors can be naturally formalized and semi-automatically proved in Coq.

Coordination models and languages play a key role in formally specifying the communication and interaction among different components in large-scale concurrent systems. In this paper, we use active learning to extract timed connector models from black-box system implementations. Firstly, parameterized Mealy machine (PMM) is introduced as an operational semantic model for channel-based coordination language Reo. With product and link operators defined, we can construct complex connectors by joining basic ones in form of PMM. Moreover, with a concretize mapping function, PMMs can be easily transformed into Mealy machines, and the latter can be extracted by an optimized L* algorithm.