Home // ICSEA 2011, The Sixth International Conference on Software Engineering Advances // View article

Invariant Preservation by Component Composition Using Semantical Interface Automata

Authors:
Sebti Mouelhi
Samir Chouali
Hassan Mountassir

Keywords: software components, interface automata, action semantics, formal correctness, invariants.

Abstract:
Component assembly is based on the verification of the compatibility between the component interface specifications. In general, these specifications do not combine the three levels of the compatibility check: behavioral protocols, signatures, and semantics of operations. In this paper, we enrich the formalism of interface automata, used to specify component protocols, by the signatures and semantics of operations. We propose a new formalism, called "semantical interface automata" (SIAs), endowed with a stronger compositional semantics than interface automata. The semantics of operations is specified by pre and post-conditions stated over their parameters and a set of variables reflecting the behavioral conduct of components interoperability. First, we show how the component compatibility is checked at the signature, semantic, and protocol levels. Second, we establish a formal methodology to check the preservation of invariants by composition of SIAs.

Pages: 305 to 311

Copyright: Copyright (c) IARIA, 2011

Publication date: October 23, 2011

Published in: conference

ISSN: 2308-4235

ISBN: 978-1-61208-165-6

Location: Barcelona, Spain

Dates: from October 23, 2011 to October 29, 2011