TU Darmstadt / ULB / tuprints

Specifying and Monitoring Non-functional Properties

Kallel, Slim :
Specifying and Monitoring Non-functional Properties.
TU Darmstadt
[Ph.D. Thesis], (2011)

[img]
Preview
PDF
thesiskallelfinal.pdf
Available under Creative Commons Attribution Non-commercial No Derivatives.

Download (1239Kb) | Preview
Item Type: Ph.D. Thesis
Title: Specifying and Monitoring Non-functional Properties
Language: English
Abstract:

This thesis focuses on the implementation and the control of non-functional safety properties during system execution. More concretely, it describes the development process of such properties, starting with the formal specification, the verification, and the runtime enforcement of the specified properties to avoid any undesired behavior.

This thesis starts by studying and classifying the approaches on the specification and runtime verification of non-functional safety properties. When examining these approaches, the following observations are made. First, the non-functional properties are generally ignored in the early phases of the software development process. They are often addressed after the functional part is implemented, which has negative effects on the quality of the code. The approaches that use UML for modeling these properties cannot verify the absence of contradictions between the specified properties. In addition, UML lacks means to express various types of non-functional properties, such as temporal properties. Second, runtime verification approaches monitor the execution of the application at runtime and detect violations of the specified properties. However, just detecting the violation is not sufficient for critical applications. These approaches should enforce these properties and avoid the misbehavior of the system by skipping the execution of undesired events. Third, in current approaches the code for enforcing non-functional properties is mostly not encapsulated in separated modules. The implementation cuts across the functional application code. This lack of modularity leads to serious problems related to the quality of code and the possibility of changing those properties.

The thesis shows a generic and holistic approach, called Seven-pro that combines formal methods and aspect-oriented programming for specifying and runtime enforcing non-functional safety properties. Seven-pro covers the whole development process of non-functional properties and avoids the gap between the specification and the implementation by automatically generating aspects from a high-level specification. The generated aspects will be integrated, in a modular way, in the functional application code for enforcing the formally specified properties at runtime.

In addition, this thesis shows how Seven-pro covers different types of non-functional properties in distributed applications. This approach is applied to structural, qualitative and quantitative behavioral non-functional properties. This thesis presents three applications for the supported types of properties.

In the context of structural properties, Seven-pro is applied for specifying and enforcing architectural properties of distributed object-oriented applications that are characterized by dynamic software architectures. Seven-pro uses a combination of Z notation and Petri nets to specify (a) the architectural styles with their architectural invariants, (b) the reconfiguration operations with their pre- and post-conditions, and (c) the coordination protocols describing the execution order of the reconfiguration operations. A verification step is performed to verify the consistency of the specification and the preservation of the architectural style after a reconfiguration of the architecture. After that, the Z and Petri nets specifications are automatically translated to AspectJ aspects to verify – before each reconfiguration operation – that all related architectural properties are satisfied.

In the context of qualitative behavioral properties, Seven-pro is applied for specifying and enforcing static and dynamic separation of duties and different types and characteristics of delegation policies on top of role-based access control. In the specification phase, TemporalZ, a combination of Z notation and linear temporal logic, is used for formally specifying the supported policies. In the verification phase, the absence of contradictions between the specified policies is verified. In the implementation phase, the aspect language Alpha is extended with a new library for supporting the specified properties. In addition, TemporalZ specifications are automatically translated to Alpha aspects to control the access permissions according to the specified policies.

In the context of quantitative behavioral properties, Seven-pro is applied for specifying and enforcing temporal properties in Web service compositions. To support both relative and absolute timed properties, a new formal language called XTUS-Automata is proposed which extends timed automata with the constructs of the XTUS language. After formally verifying the absence of deadlocks in timed automata specifications and verifying other properties related to the XTUS language, the XTUS-Automata specifications are automatically translated to AO4BPEL aspects.

Alternative Abstract:
Alternative AbstractLanguage
Schwerpunkt dieser Dissertation ist die Implementierung und Durchsetzung von nicht-funktionalen Sicherheitseigenschaften während der Programmausführung. Konkret wird ein Entwicklungsprozess beschrieben, der sicherstellt, dass die Software die gewünschten Eigenschaften aufweist. Dieser reicht von der formalen Spezifikation über die Verifikation bis zur Durchsetzung der spezifizierten Eigenschaften zur Laufzeit. Dies ermöglicht es unerwünschtes Verhalten zu vermeiden. Diese Dissertation beginnt mit einer Studie und Klassifikation der Ansätze zur Spezifikation und Laufzeitverifikation von nicht-funktionalen Sicherheitseigenschaften. Dabei wurden folgende Beobachtungen gemacht: Erstens werden nicht-funktionale Eigenschaften während der frühen Phasen des Softwareentwicklungsprozesses weitestgehend ignoriert; sie werden meist erst berücksichtigt, wenn der funktionale Teil bereits implementiert ist was sich negativ auf die Codequalität auswirkt. Die Ansätze, die UML zur Modellierung dieser Eigenschaften benutzen, können die Widerspruchsfreiheit bezüglich der spezifizierten Eigenschaften nicht beweisen. Des Weiteren fehlt es der UML an Möglichkeiten verschiedene Arten nicht-funktionaler Eigenschaften, wie z.B. zeitbezogene Eigenschaften, auszudrücken. Zweitens, Ansätze, die das Verhalten der Anwendung zur Laufzeit beobachten und verifizieren und dadurch Verletzungen detektieren, sind im Falle kritischer Anwendungen nicht ausreichend. Solche Ansätze sollten die geforderten Eigenschaften durchsetzen und ein Systemfehlverhalten durch Unterdrücken der Ausführung unerwünschter Ereignisse vermeiden. Drittens, der Code zur Durchsetzung der nicht-funktionalen Anforderungen ist in aktuellen Ansätzen nicht gut modularisiert. Die Implementierung durchschneidet vielmehr den funktionalen Kern der Anwendung. Dieser Mangel an Modularität führt zu schwerwiegenden Problemen bezüglich der Codequalität und der Änderbarkeit der Sicherheitsanforderungen. Diese Dissertation verfolgt einen generischen, holistischen Ansatz namens Seven-pro, der formale Methoden und aspekt-orientierte Programmierung kombiniert, um nicht-funktionale Sicherheitsanforderungen sowohl zu spezifizieren als auch durchzusetzen. Seven-pro deckt den gesamten Entwicklungsprozess nicht-funktionaler Anforderungen ab und vermeidet Diskrepanzen zwischen Spezifikation und Implementierung durch das automatische Generieren von Aspekten basierend auf der Spezifikation. Die generierten Aspekte werden auf modulare Art und Weise mit dem funktionalen Kern der Anwendung integriert, um die formal spezifizierten Eigenschaften zur Laufzeit durchzusetzen. Zusätzlich zeigt diese Dissertation, wie Seven-pro verschiedene Arten von funktionalen Anforderungen im Kontext verteilter Anwendungen abdeckt. Der Ansatz wird dabei auf strukturelle, qualitative und quantitative nicht-funktionale Eigenschaften des Verhaltens angewendet. Die Arbeit präsentiert drei Anwendungen für die unterstützten Arten von Eigenschaften. Im Kontext struktureller Eigenschaften wird Seven-pro zur Spezifikation und Durchsetzung architektonischer Eigenschaften von verteilten, objekt-orientierten Anwendungen angewandt welche eine dynamische Softwarearchitektur aufweisen. Seven-pro verwendet eine Kombination aus Z-Notation und Petrinetzen zur Spezifikation (a) des Architekturstils und von Architekturinvarianten, (b) der Rekonfigurationsoptionen mit Vor- und Nachbedingung, sowie (c) der Protokolle zur Koordination der Reihenfolge der Rekonfigurationsoperationen. Ein Verifikationsschritt wird durchgeführt, um die Konsistenz der Spezifikation und den Erhalt des Architekturstils nach deren Rekonfiguration sicherzustellen. Daran anschließend werden die Z- und Petrinetzspezifikationen automatisch in AspectJ-Aspekte übersetzt, um vor jeder Rekonfigurationsoperation sicherzustellen, das alle zugehörigen Architektureigenschaften erfüllt sind. Im Kontext qualitativer Verhaltenseigenschaften wird Seven-pro eingesetzt zur Spezifikation und Durchsetzung statischer und dynamischer Aufgabentrennungs- und Delegationsrichtlinien auf Basis von rollenbasierten Zugangsbeschränkungen. Während der Spezifikationsphase wird TemporalZ, eine Kombination aus Z-Notation und linearer Temporallogik benutzt, um die unterstützten Richtlinien formal zu beschreiben. Während der Verifikationsphase werden die spezifizierten Richtlinien auf Widerspruchsfreiheit geprüft. In der Implementierungsphase wird die Aspektsprache Alpha mit einer neuen Bibliothek, die die spezifizierten Eigenschaften unterstützt, erweitert. Des weiteren werden TemporalZ-Spezifikationen automatisch in Alpha-Aspekte übersetzt, die Zugriffsrechte gemäß der spezifizierten Richtlinien beschränken. Im Kontext quantitativer Verhaltenseigenschaften wird Seven-pro zur Spezifikation und Durchsetzung zeitbezogener Eigenschaften einer Komposition von Web Services eingesetzt. Um sowohl relative als auch absolute zeitbezogene Eigenschaften zu unterstützen, wird eine neue formale Sprache mit dem Namen XTUS-Automata vorgeschlagen, die zeitbezogene Automaten um die Konstrukte der XTUS-Sprache erweitert. Nachdem sowohl die Deadlock-Freiheit als auch andere, XTUS-bezogene Eigenschaften bewiesen worden sind, werden die XTUS-Automata-Spezifikationen automatisch in AO4BPEL-Aspekte übersetzt.German
Classification DDC: 000 Allgemeines, Informatik, Informationswissenschaft > 004 Informatik
Divisions: Fachbereich Informatik > Softwaretechnik
Date Deposited: 20 Jul 2011 11:05
Last Modified: 07 Dec 2012 12:00
URN: urn:nbn:de:tuda-tuprints-26770
License: Creative Commons: Attribution-Noncommercial-No Derivative Works 3.0
Referees: Mezini, Prof. Mira and Jmaiel, Prof. Mohamed and Südholt, Prof. Mario
Refereed: 11 July 2011
URI: http://tuprints.ulb.tu-darmstadt.de/id/eprint/2677
Export:

Actions (login required)

View Item View Item