Kallel, Slim ; Charfi, Anis ; Mezini, Mira ; Jmaiel, Mohamed (2007)
Combining Formal Methods and Aspects for Specifying and Enforcing Architectural Invariants.
In: Coordination Models and Languages
doi: 10.1007/978-3-540-72794-1_12
Buchkapitel, Bibliographie
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 |
| Art des Eintrags: | Bibliographie |
| Titel: | Combining Formal Methods and Aspects for Specifying and Enforcing Architectural Invariants |
| Sprache: | Englisch |
| Publikationsjahr: | 2007 |
| Ort: | Heidelberg/Berlin, Germany |
| Buchtitel: | Coordination Models and Languages |
| Reihe: | Lecture Notes In Computer Science |
| Band einer Reihe: | 4467 |
| Veranstaltungstitel: | 9th International Conference on Coordination Models and Languages (Coordination '07) |
| DOI: | 10.1007/978-3-540-72794-1_12 |
| 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. |
| Fachbereich(e)/-gebiet(e): | 20 Fachbereich Informatik 20 Fachbereich Informatik > Softwaretechnik |
| Hinterlegungsdatum: | 14 Sep 2009 07:22 |
| Letzte Änderung: | 05 Mär 2013 09:22 |
| PPN: | |
| Export: | |
| Suche nach Titel in: | TUfind oder in Google |
 |
Frage zum Eintrag |
Optionen (nur für Redakteure)
 |
Redaktionelle Details anzeigen |
Drucken
Impressum