Home > Research > Publications & Outputs > From Aspectual Requirements to Proof Obligation...

Research

Associated organisational unit

Links

Text available via DOI:

View graph of relations

From Aspectual Requirements to Proof Obligations for Aspect-Oriented Systems

Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSN › Conference contribution/Paper › peer-review

Published

Standard

From Aspectual Requirements to Proof Obligations for Aspect-Oriented Systems. / Katz, Shmuel; Rashid, Awais.
12th IEEE International Requirements Engineering Conference (RE'04). Washington, DC, USA: IEEE Computer Society, 2004. p. 48-57.

Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSN › Conference contribution/Paper › peer-review

Harvard

Katz, S & Rashid, A 2004, From Aspectual Requirements to Proof Obligations for Aspect-Oriented Systems. in 12th IEEE International Requirements Engineering Conference (RE'04). IEEE Computer Society, Washington, DC, USA, pp. 48-57. https://doi.org/10.1109/ICRE.2004.1335663

APA

Katz, S., & Rashid, A. (2004). From Aspectual Requirements to Proof Obligations for Aspect-Oriented Systems. In 12th IEEE International Requirements Engineering Conference (RE'04) (pp. 48-57). IEEE Computer Society. https://doi.org/10.1109/ICRE.2004.1335663

Vancouver

Katz S, Rashid A. From Aspectual Requirements to Proof Obligations for Aspect-Oriented Systems. In 12th IEEE International Requirements Engineering Conference (RE'04). Washington, DC, USA: IEEE Computer Society. 2004. p. 48-57 doi: 10.1109/ICRE.2004.1335663

Author

Katz, Shmuel ; Rashid, Awais. / From Aspectual Requirements to Proof Obligations for Aspect-Oriented Systems. 12th IEEE International Requirements Engineering Conference (RE'04). Washington, DC, USA : IEEE Computer Society, 2004. pp. 48-57

Bibtex

@inproceedings{85e251a4c71d4edfbe39552a569d932b,
title = "From Aspectual Requirements to Proof Obligations for Aspect-Oriented Systems",
abstract = "Aspect-oriented software development (AOSD) techniques support systematic modularization and composition of crosscutting concerns. Though AOSD techniques have been proposed to handle crosscutting concerns at various stages during the software life cycle, there is a traceability gap between the aspects at the requirements level and those at later development stages. It is not clear what proof obligations about an aspect-oriented implementation follow from the initial aspectual requirements.This paper presents PROBE, a framework for generation of proof obligations for aspect-oriented systems from the initial aspectual requirements and associated trade-offs. The abstract proof obligations are expressed in standard linear temporal logic. Key components of the framework include an extended Ontology with parametric temporal formulas and functions, and extensive treatment of conflicts among requirements. The resultant temporal logic assertions, grouped into specifications of aspect implementations, can then be instantiated in terms of the implementation and verification tools.",
author = "Shmuel Katz and Awais Rashid",
year = "2004",
doi = "10.1109/ICRE.2004.1335663",
language = "English",
isbn = "0-7695-2174-6",
pages = "48--57",
booktitle = "12th IEEE International Requirements Engineering Conference (RE'04)",
publisher = "IEEE Computer Society",

}

RIS

TY - GEN

T1 - From Aspectual Requirements to Proof Obligations for Aspect-Oriented Systems

AU - Katz, Shmuel

AU - Rashid, Awais

PY - 2004

Y1 - 2004

N2 - Aspect-oriented software development (AOSD) techniques support systematic modularization and composition of crosscutting concerns. Though AOSD techniques have been proposed to handle crosscutting concerns at various stages during the software life cycle, there is a traceability gap between the aspects at the requirements level and those at later development stages. It is not clear what proof obligations about an aspect-oriented implementation follow from the initial aspectual requirements.This paper presents PROBE, a framework for generation of proof obligations for aspect-oriented systems from the initial aspectual requirements and associated trade-offs. The abstract proof obligations are expressed in standard linear temporal logic. Key components of the framework include an extended Ontology with parametric temporal formulas and functions, and extensive treatment of conflicts among requirements. The resultant temporal logic assertions, grouped into specifications of aspect implementations, can then be instantiated in terms of the implementation and verification tools.

AB - Aspect-oriented software development (AOSD) techniques support systematic modularization and composition of crosscutting concerns. Though AOSD techniques have been proposed to handle crosscutting concerns at various stages during the software life cycle, there is a traceability gap between the aspects at the requirements level and those at later development stages. It is not clear what proof obligations about an aspect-oriented implementation follow from the initial aspectual requirements.This paper presents PROBE, a framework for generation of proof obligations for aspect-oriented systems from the initial aspectual requirements and associated trade-offs. The abstract proof obligations are expressed in standard linear temporal logic. Key components of the framework include an extended Ontology with parametric temporal formulas and functions, and extensive treatment of conflicts among requirements. The resultant temporal logic assertions, grouped into specifications of aspect implementations, can then be instantiated in terms of the implementation and verification tools.

U2 - 10.1109/ICRE.2004.1335663

DO - 10.1109/ICRE.2004.1335663

M3 - Conference contribution/Paper

SN - 0-7695-2174-6

SP - 48

EP - 57

BT - 12th IEEE International Requirements Engineering Conference (RE'04)

PB - IEEE Computer Society

CY - Washington, DC, USA

ER -