TU Darmstadt / ULB / TUbiblio

Combining Formal Methods and Aspects for Specifying and Enforcing Architectural Invariants

Kallel, Slim and Charfi, Anis and Mezini, Mira and Jmaiel, Mohamed (2007):
Combining Formal Methods and Aspects for Specifying and Enforcing Architectural Invariants.
In: Coordination Models and Languages, Heidelberg/Berlin, Germany, pp. 211-230, [Online-Edition: http://www.springerlink.com/content/617246q4143160q4/],
[Book Section]

Abstract

Several types of invariants should be maintained when the architecture of a software application evolves. To specify these invariants in a reliable way, formal methods are used. However, current approaches suffer from two limitations. First, they support only certain types of invariants. Second, checking and enforcing the invariants is generally done by adding appropriate logic to the application implementation in a manual way, which is error-prone and may lead to architectural erosion. In this paper, we combine the Z notation and Petri nets to specify formally architectural invariants in distributed object-oriented software applications. Moreover, we use a generative aspect-based approach to checking and enforcing these invariants. Thus, we bridge the gap between the formal specification and the implementation. Our approach brings several other benefits as the code that checks and enforces invariants is generated automatically and well-modularized in aspects.

Item Type: Book Section
Erschienen: 2007
Creators: Kallel, Slim and Charfi, Anis and Mezini, Mira and Jmaiel, Mohamed
Title: Combining Formal Methods and Aspects for Specifying and Enforcing Architectural Invariants
Language: English
Abstract:

Several types of invariants should be maintained when the architecture of a software application evolves. To specify these invariants in a reliable way, formal methods are used. However, current approaches suffer from two limitations. First, they support only certain types of invariants. Second, checking and enforcing the invariants is generally done by adding appropriate logic to the application implementation in a manual way, which is error-prone and may lead to architectural erosion. In this paper, we combine the Z notation and Petri nets to specify formally architectural invariants in distributed object-oriented software applications. Moreover, we use a generative aspect-based approach to checking and enforcing these invariants. Thus, we bridge the gap between the formal specification and the implementation. Our approach brings several other benefits as the code that checks and enforces invariants is generated automatically and well-modularized in aspects.

Title of Book: Coordination Models and Languages
Series Name: Lecture Notes In Computer Science
Volume: 4467
Place of Publication: Heidelberg/Berlin, Germany
Divisions: 20 Department of Computer Science
20 Department of Computer Science > Software Technology
Event Title: 9th International Conference on Coordination Models and Languages (Coordination '07)
Date Deposited: 14 Sep 2009 07:22
Official URL: http://www.springerlink.com/content/617246q4143160q4/
Identification Number: doi:10.1007/978-3-540-72794-1_12
Export:
Suche nach Titel in: TUfind oder in Google

Optionen (nur für Redakteure)

View Item View Item