Fundamenta Informaticae - Volume 82, issue 4

Article Type: Other

Citation: Fundamenta Informaticae, vol. 82, no. 4, pp. i-i, 2008

Authors: Stehr, Mark-Oliver

Article Type: Research Article

Abstract: The design of complex software systems fundamentally relies on the understanding of abstract components and their interactions. Although compositional techniques are being successfully employed in practice, the use of such techniques is often rather informal and intuitive, and typically a justification for correct behaviour of the composed system exists but is not expressed explicitly. In this paper, we show what can be gained from treating such justifications as first-class citizens. The fairly general setting for …this paper is a formal development of a UNITY-style temporal logic for labeled transition systems in the calculus of inductive constructions which has been conducted using the Coq proof assistant in a formally rigorous way. Our development not only subsumes the original UNITY approach to program verification and the more recent approach of New UNITY, but goes beyond it in several essential aspects, such as the generality of the program/system model (arbitrary labeled transition systems instead of UNITY programs), the notion of fairness (weak group fairness instead of unconditional fairness), and the issue of compositionality (not only for safety but also for liveness assertions). The last aspect, which we feel is crucial in the foundations for software engineering, is subject of this paper. We present a general proof rule for compositional verification of liveness assertions in tightly coupled systems. It relies on a notion of compositional proofs, which in turn is closely related to classical work on interference-free proofs for parallel programs. The formulation of this new proof rule and the verification of its soundness does not only exploit the strong inductive reasoning capabilities of the calculus of inductive constructions, but it also uses the propositions-as-types interpretation and the associated proofs-as-objects interpretation in an essential way. Show more

Citation: Fundamenta Informaticae, vol. 82, no. 4, pp. 311-340, 2008

Authors: Johnsen, Einar Broch | Owe, Olaf | Torjusen, Arild B.

Article Type: Research Article

Abstract: Many distributed applications can be understood in terms of components interacting in an open environment such as the Internet. Open environments are subject to change in unpredictable ways, as applications may arrive, evolve, or disappear. In order to validate components in such environments, it can be useful to build simulation environments which reflect this highly unpredictable behavior. This paper considers the validation of components with respect to behavioral interfaces. Behavioral interfaces specify …semantic requirements on the observable behavior of components, expressed in an assume-guarantee style. In our approach, a rewriting logic model is transparently extended with the history of all observable communications, and metalevel strategies are used to guide the simulation of environment behavior. Over-specification of the environment is avoided by allowing arbitrary environment behavior within the bounds of the assumption on observable behavior, while the component is validated with respect to the guarantee of the behavioral interface. Show more

Keywords: Validation, components, behavioral interfaces, adaptive testing, rewriting logic

Citation: Fundamenta Informaticae, vol. 82, no. 4, pp. 341-359, 2008

Authors: Clarke, Dave

Article Type: Research Article

Abstract: Software systems evolve over time. From a component-based software engineering perspective, this means that either the components of the system need to change, or, if components are connected using a coordination layer, then the way in which they are connected needs to change, or both. In some situations, changes must be performed without stopping the running system. This not only introduces a serious technological challenge, it also makes reasoning about the evolving system difficult. One approach …to this problem is to use component connectors to plug components together. Reconfiguration of a system can then be reduced to reconfiguring the component connector, as changing component implementations can be implemented by changing which components the connector connects together. The coordination language Reo offers operations to dynamically reconfigure the topology of component connectors, but until now, no means for reasoning about reconfiguration in Reo has been developed. This issue is addressed in this paper. To enable reasoning about connector behaviour, and hence behaviour of the composed system, we present a semantics of Reo in the presence of reconfiguration, and a logic together with its model checking algorithm. Show more

Keywords: Dynamic Reconfiguration, Coordination, Component Connectors, Reo

Citation: Fundamenta Informaticae, vol. 82, no. 4, pp. 361-390, 2008

Authors: Ábrahám, Erika | de Boer, Frank S. | de Roever, Willem-Paul | Steffen, Martin

Article Type: Research Article

Abstract: Besides the features of a class-based object-oriented language, Java integrates concurrency via its thread-classes, allowing for a multithreaded flow of control. Besides that, the language offers a flexible exception mechanism for handling errors or exceptional program conditions. To reason about safety-properties of Java-programs and extending previous work on the proof theory for monitor synchronization, we introduce in this paper an assertional proof method for JavaMT ("Multi-Threaded Java"), a small concurrent …sublanguage of Java, covering concurrency and especially exception handling. We show soundness and relative completeness of the proof method. Show more

Citation: Fundamenta Informaticae, vol. 82, no. 4, pp. 391-463, 2008

Authors: Esmaeilsabzali, Shahram | Day, Nancy A. | Mavaddat, Farhad

Article Type: Research Article

Abstract: Many formalisms use interleaving to model concurrency. To describe some system behaviours appropriately, we need to limit interleaving. For example, in a component-based system, we might wish to limit interleaving to force the inputs to a method to arrive together in order. InWeb services, the arrival of XML messages consisting of multiple simple parts should not be interleaved with the behaviour of another component. We introduce interface automata with complex actions (IACA), which adds complex actions …to de Alfaro and Henzinger's interface automata (IA). A complex action is a sequence of actions that may not be interleaved with actions from other components. The composition operation and refinement relation are more involved in IACA compared to IA, and we must sacrifice associativity of composition. However, we argue that the advantages of having complex actions make it a useful formalism. We provide proofs of various properties of IACA and discuss the use of IACA for modellingWeb services. Show more

Citation: Fundamenta Informaticae, vol. 82, no. 4, pp. 465-512, 2008