This paper addresses a classical problem of distributed computing: Given a labelled transition system (LTS), how to synthesise a distributed labelled transition system (DLTS) such that the global behaviour of the DLTS is isomorphic to the given LTS. It has been proved that it is not possible to synthesise a DLTS for every LTS. Only LTSs that satisfy certain conditions are distributable. These conditions are complex and difficult to understand. This paper contributes by showing how to encode a propositional logic formula against a given LTS. The formula thus encoded is satisfiable if and only if the LTS is distributable. The satisfiability of the encoded formula can be determined automatically using SAT solvers.

Input-output labelled transition system (IOLTS) is a state-based model that is widely used to describe the functional behaviour of a reactive system. However when the same system is observed asynchronously through a pair of unbounded FIFO queues (or channels), its apparent behaviour is different from its actual behaviour. This is because an execution trace of the system could appear distorted in a multitude of ways. The apparent behaviour is called the asynchronous behaviour of the system. It is well known that the asynchronous behaviour can also be described by an infinite-state IOLTS. This description however proves to be appropriate only as long as the channels are assumed to be reliable. The moment we throw in unreliability assumptions, the asynchronous behaviour becomes probabilistic in nature. The plain IOLTS model is simply not expressive enough to capture this probabilistic behaviour. To this end, we in this paper show how the asynchronous behaviour of a reactive system can be captured by Segala's probabilistic automata (SPA). We further show how the SPA expressing the asynchronous behaviour can serve as a reference model for probabilistic testing of asynchronously communicating systems.

In this paper, we propose a new semantic equivalence over the set of probabilistic processes. This equivalence is defined by means of asynchronous testing. We show that each probabilistic process exhibits a certain input-output behaviour when subjected to asynchronous testing. Two processes are said to be semantically equivalent when they exhibit the same behaviour. There already exists a notion of semantic equivalence defined through synchronous testing. We finally draw comparison between the equivalence proposed by us and the existing equivalence.

Cyber-physical systems (CPSs) are digital real-time systems embedded in analog environments. A typical example of a CPS is a control program for an industrial plant. While the program can be in any one of the finite number of discrete states, the physical quantities of the plant evolve continuously in each state according to the physical laws. Such systems are usually safety-critical and therefore their correctness is a prime concern. However verifying these systems for correctness is far from trivial. The challenge comes from the fact that the discrete-continuous combine dynamics give rise to an uncountable number of states. To this end, in this paper we suggest an approach for conformance testing of CPSs. Our approach is based on modeling the given CPS as a hybrid automaton.

The paper relooks at one of the classical problems in distributed computing: Given a labelled transition system (LTS), how to synthesize a distributed labelled transition system (DLTS) such that the global behaviour of the DLTS is equivalent to that of the given LTS. This problem has been addressed for various notions of behavioral equivalences, viz., isomorphism, language equivalence, bisimulation, etc. For all these equivalences it has been found that a DLTS cannot be synthesized for every given LTS. This holds true even if the given LTS is assumed to be acyclic. Here we address the same problem with respect to the relation Conf. This relation is not an equivalence. It is rather a preorder that is used to define the notion of conformance in the context of conformance testing [2]. We show that synthesizing a DLTS with respect to conformance has two big advantages. First, a DLTS can be synthesized for every given acyclic LTS. Secondly, a DLTS thus synthesized can be verified for correctness in a distributed and concurrent manner.

Conformance testing has a rich underlying theory popularly called IOCO-test theory. In the realm of IOCO-test theory, this paper addresses the issue of testing a component of an asynchronously communicating distributed system. Testing a system which communicates asynchronously (i.e., through some medium) with its environment is more difficult than testing a system which communicates synchronously (i.e., directly without any medium). What impedes asynchronous testing is that the actual behavior of the implementation under test (IUT) appears distorted and infinite to the tester. This impediment consequently renders the problem of generating a complete test suite, from the given specification of the IUT, infeasible. To this end, this paper contributes by proposing a tagging protocol which when implemented by the asynchronously communicating distributed system will make the problem of generating a complete test suite, from the specification of any of its component, feasible. Further, this paper describes how to generate the test suite from the given specification of the component.

IOLTS (input output labeled transition system) is a versatile model and is frequently used in model based testing to model the functional behavior of an IUT (implementation under test). However when a system is tested remotely, its observed behavior can be different from its actual functional behavior. In [2], we defined a notion of remotely observed behavior of an IOLTS in terms of its actual behavior. This paper contributes by proposing a methodology to simulate a PDA (push down automaton) from the given IOLTS such that the simulated PDA precisely expresses the remotely observed behavior of the IOLTS. The simulated PDA can be thought of as an automatic test generator for remote testing.

The only practical way to test distributed message-passing systems is to use local testing. In this approach, used in formalisms such as concurrent TTCN-3, some components are replaced by test processes. Local testing consists of monitoring the interactions between these test processes and the rest of the system and comparing these observations with the specification, typically described in terms of message sequence charts. The main difficulty with this approach is that local observations can combine in unexpected ways to define implied scenarios not present in the original specification. Checking for implied scenarios is known to be undecidable for regular specifications, even if observations are made for all but one process at a time. We propose an approach where we append tags to the messages generated by the system under test. Our tags are generated in a uniform manner, without referring to or influencing the internal details of the underlying system. These enriched behaviours are then compared against a tagged version of the specification. Our main result is that detecting implied scenarios becomes decidable in the presence of tagging.