TU Darmstadt / ULB / TUbiblio

Combining Formal Methods and Aspects for Specifying and Enforcing Architectural Invariants

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

Offizielle URL: http://www.springerlink.com/content/617246q4143160q4/

Kurzbeschreibung (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.

Typ des Eintrags: Buchkapitel
Erschienen: 2007
Autor(en): Kallel, Slim ; Charfi, Anis ; Mezini, Mira ; Jmaiel, Mohamed
Titel: Combining Formal Methods and Aspects for Specifying and Enforcing Architectural Invariants
Sprache: Englisch
Kurzbeschreibung (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.

Buchtitel: Coordination Models and Languages
Reihe: Lecture Notes In Computer Science
Band: 4467
Ort: Heidelberg/Berlin, Germany
Fachbereich(e)/-gebiet(e): 20 Fachbereich Informatik
20 Fachbereich Informatik > Softwaretechnik
Veranstaltungstitel: 9th International Conference on Coordination Models and Languages (Coordination '07)
Hinterlegungsdatum: 14 Sep 2009 07:22
Offizielle URL: http://www.springerlink.com/content/617246q4143160q4/
ID-Nummer: doi:10.1007/978-3-540-72794-1_12
Export:

Optionen (nur für Redakteure)

Eintrag anzeigen Eintrag anzeigen