Incremental construction of systems: An efficient characterization of the lacking sub-system

Software engineering research is driven by the aim of making software development more dynamic, flexible and evolvable. Nowadays the emphasis is on the evolution of pre-existing sub-systems and component and service-based development, where often only a part of the system is totally under control of the designer, most components being remotely operated by external vendors. In this context, we tackle the following problem: given the formal specification of the (incomplete) system, say it p, already built, how to characterize collaborators of p to be selected, based on a given communication interface L, so that a given property φ is satisfied. Using properties described by temporal logic formulae and systems by CCS processes, if φ is the formula to be satisfied by the complete system, an efficient and automatic procedure is defined to identify a formula ψ such that, for each existing process q satisfying ψ, the process (p∣q)∖L satisfies φ. Important features of this result are simplicity of the derived property ψ, compared to the original one, and scalability of the verification process. Such characteristics are necessary for applying the method to both incremental design and system evolution scenarios where p is already in place, and one needs to understand the specification of the functionality of the new component that should correctly interact with p. Indeed, in general, finding a suitable partner for p is easier than finding a complete system satisfying the global property. Moreover, in this paper it is shown how ψ can be used also to select a set of possible candidate processes q through a property-directed and structural heuristic. From the verification point of view, the description of the lacking component through a logic formula guarantees correctness of the integration with p of any process that exhibits a behaviour compliant with the inferred formula.