The process of completing, correcting and prioritising specifications is an essential but very complex task for the maintenance and improvement of software systems. The preservation of functionalities and the ability to accommodate changes are main objectives of the software development cycle to guarantee system reliability. Logical theories able to fully model such processes are still insufficient. In this paper we propose a full formalisation of such operations on software systems inspired by the Alchourrón–Gärdenfors–Makinson (AGM) paradigm for belief revision of human epistemic states. We represent specifications as finite sets of formulas equipped with a priority relation that models functional entrenchment of properties. We propose to handle specification incompleteness through ordered expansion, inconsistency through ordered safe contraction and prioritisation through revision with reordering, and model all three in an algorithmic fashion. We show how the system satisfies basic properties of the AGM paradigm, including Levi’s and Harper’s identities. We offer a concrete example and complexity results for the inference and model checking problems on revision. We conclude by describing resilience and evolvability of software systems based on such revision operators.
A theory of change for prioritised resilient and evolvable software systems / G. Primiero, F. Raimondi, T. Chen. - In: SYNTHESE. - ISSN 0039-7857. - 198:Suppl. 23 Special Issue(2021 Oct), pp. 5719-5744. [10.1007/s11229-019-02305-7]
A theory of change for prioritised resilient and evolvable software systems
G. Primiero
Primo
;
2021
Abstract
The process of completing, correcting and prioritising specifications is an essential but very complex task for the maintenance and improvement of software systems. The preservation of functionalities and the ability to accommodate changes are main objectives of the software development cycle to guarantee system reliability. Logical theories able to fully model such processes are still insufficient. In this paper we propose a full formalisation of such operations on software systems inspired by the Alchourrón–Gärdenfors–Makinson (AGM) paradigm for belief revision of human epistemic states. We represent specifications as finite sets of formulas equipped with a priority relation that models functional entrenchment of properties. We propose to handle specification incompleteness through ordered expansion, inconsistency through ordered safe contraction and prioritisation through revision with reordering, and model all three in an algorithmic fashion. We show how the system satisfies basic properties of the AGM paradigm, including Levi’s and Harper’s identities. We offer a concrete example and complexity results for the inference and model checking problems on revision. We conclude by describing resilience and evolvability of software systems based on such revision operators.File | Dimensione | Formato | |
---|---|---|---|
softwaretheorychange_finalrevision_public.pdf
Open Access dal 01/01/2021
Tipologia:
Post-print, accepted manuscript ecc. (versione accettata dall'editore)
Dimensione
400.64 kB
Formato
Adobe PDF
|
400.64 kB | Adobe PDF | Visualizza/Apri |
Primiero2019_Article_ATheoryOfChangeForPrioritisedR.pdf
accesso riservato
Tipologia:
Publisher's version/PDF
Dimensione
1.06 MB
Formato
Adobe PDF
|
1.06 MB | Adobe PDF | Visualizza/Apri Richiedi una copia |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.