Software that meets its Intent

Marieke  Huisman; Herbert Bos; Sjaak Brinkkemper; Arie van Deursen; Jan Friso Groote; Patricia Lago; Jaco  van de Pol; Eelco Visser

doi:10.1007/978-3-319-47169-3_47

Software that meets its Intent

Marieke Huisman, Herbert Bos, Sjaak Brinkkemper, Arie van Deursen, Jan Friso Groote, Patricia Lago, Jaco van de Pol, Eelco Visser

Formal Methods and Tools

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

2 Citations (Scopus)

10 Downloads (Pure)

Abstract

Software is widely used, and society increasingly depends on its reliability. However, software has become so complex and it evolves so quickly that we fail to keep it under control. Therefore, we propose intents: fundamental laws that capture a software systems’ intended behavior (resilient, secure, safe, sustainable, etc.). The realization of this idea requires novel theories, algorithms, tools, and techniques to discover, express, verify, and evolve software intents. Thus, future software systems will be able to verify themselves that they meet their intents. Moreover, they will be able to respond to deviations from intents through self-correction. In this article we propose a research agenda, outlining which novel theories, algorithms and tools are required.

Original language	English
Title of host publication	Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications
Subtitle of host publication	7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10-14, 2016, Proceedings, Part II
Editors	Tiziana Margaria, Bernhard Steffen
Publisher	Springer
Pages	609-625
Number of pages	17
ISBN (Electronic)	978-3-319-47169-3
ISBN (Print)	978-3-319-47168-6
DOIs	https://doi.org/10.1007/978-3-319-47169-3_47
Publication status	Published - Oct 2016
Event	7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2016 - Corfu, Greece Duration: 10 Oct 2016 → 14 Oct 2016 Conference number: 7 http://www.isola-conference.org/isola2016/

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	9953
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2016
Abbreviated title	ISoLA 2016
Country/Territory	Greece
City	Corfu
Period	10/10/16 → 14/10/16
Internet address	http://www.isola-conference.org/isola2016/

Keywords

Model checker
Satisfiability modulo theory
Intended behavior
Program verifier
Proof checker

Access to Document

10.1007/978-3-319-47169-3_47

Cite this

Huisman, M., Bos, H., Brinkkemper, S., van Deursen, A., Groote, J. F., Lago, P., van de Pol, J., & Visser, E. (2016). Software that meets its Intent. In T. Margaria, & B. Steffen (Eds.), Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications: 7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10-14, 2016, Proceedings, Part II (pp. 609-625). (Lecture Notes in Computer Science; Vol. 9953). Springer. https://doi.org/10.1007/978-3-319-47169-3_47

Huisman, Marieke ; Bos, Herbert ; Brinkkemper, Sjaak et al. / Software that meets its Intent. Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications: 7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10-14, 2016, Proceedings, Part II. editor / Tiziana Margaria ; Bernhard Steffen. Springer, 2016. pp. 609-625 (Lecture Notes in Computer Science).

@inproceedings{cec6a17f08f14b6abce7de126b103137,

title = "Software that meets its Intent",

abstract = "Software is widely used, and society increasingly depends on its reliability. However, software has become so complex and it evolves so quickly that we fail to keep it under control. Therefore, we propose intents: fundamental laws that capture a software systems{\textquoteright} intended behavior (resilient, secure, safe, sustainable, etc.). The realization of this idea requires novel theories, algorithms, tools, and techniques to discover, express, verify, and evolve software intents. Thus, future software systems will be able to verify themselves that they meet their intents. Moreover, they will be able to respond to deviations from intents through self-correction. In this article we propose a research agenda, outlining which novel theories, algorithms and tools are required.",

keywords = "Model checker, Satisfiability modulo theory, Intended behavior, Program verifier, Proof checker",

author = "Marieke Huisman and Herbert Bos and Sjaak Brinkkemper and {van Deursen}, Arie and Groote, {Jan Friso} and Patricia Lago and {van de Pol}, Jaco and Eelco Visser",

year = "2016",

month = oct,

doi = "10.1007/978-3-319-47169-3_47",

language = "English",

isbn = "978-3-319-47168-6",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "609--625",

editor = "Tiziana Margaria and Bernhard Steffen",

booktitle = "Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications",

address = "Germany",

note = "7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2016, ISoLA 2016 ; Conference date: 10-10-2016 Through 14-10-2016",

url = "http://www.isola-conference.org/isola2016/",

}

Huisman, M, Bos, H, Brinkkemper, S, van Deursen, A, Groote, JF, Lago, P, van de Pol, J & Visser, E 2016, Software that meets its Intent. in T Margaria & B Steffen (eds), Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications: 7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10-14, 2016, Proceedings, Part II. Lecture Notes in Computer Science, vol. 9953, Springer, pp. 609-625, 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2016, Corfu, Greece, 10/10/16. https://doi.org/10.1007/978-3-319-47169-3_47

Software that meets its Intent. / Huisman, Marieke ; Bos, Herbert; Brinkkemper, Sjaak et al.
Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications: 7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10-14, 2016, Proceedings, Part II. ed. / Tiziana Margaria; Bernhard Steffen. Springer, 2016. p. 609-625 (Lecture Notes in Computer Science; Vol. 9953).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Software that meets its Intent

AU - Huisman, Marieke

AU - Bos, Herbert

AU - Brinkkemper, Sjaak

AU - van Deursen, Arie

AU - Groote, Jan Friso

AU - Lago, Patricia

AU - van de Pol, Jaco

AU - Visser, Eelco

N1 - Conference code: 7

PY - 2016/10

Y1 - 2016/10

N2 - Software is widely used, and society increasingly depends on its reliability. However, software has become so complex and it evolves so quickly that we fail to keep it under control. Therefore, we propose intents: fundamental laws that capture a software systems’ intended behavior (resilient, secure, safe, sustainable, etc.). The realization of this idea requires novel theories, algorithms, tools, and techniques to discover, express, verify, and evolve software intents. Thus, future software systems will be able to verify themselves that they meet their intents. Moreover, they will be able to respond to deviations from intents through self-correction. In this article we propose a research agenda, outlining which novel theories, algorithms and tools are required.

AB - Software is widely used, and society increasingly depends on its reliability. However, software has become so complex and it evolves so quickly that we fail to keep it under control. Therefore, we propose intents: fundamental laws that capture a software systems’ intended behavior (resilient, secure, safe, sustainable, etc.). The realization of this idea requires novel theories, algorithms, tools, and techniques to discover, express, verify, and evolve software intents. Thus, future software systems will be able to verify themselves that they meet their intents. Moreover, they will be able to respond to deviations from intents through self-correction. In this article we propose a research agenda, outlining which novel theories, algorithms and tools are required.

KW - Model checker

KW - Satisfiability modulo theory

KW - Intended behavior

KW - Program verifier

KW - Proof checker

U2 - 10.1007/978-3-319-47169-3_47

DO - 10.1007/978-3-319-47169-3_47

M3 - Conference contribution

SN - 978-3-319-47168-6

T3 - Lecture Notes in Computer Science

SP - 609

EP - 625

BT - Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications

A2 - Margaria, Tiziana

A2 - Steffen, Bernhard

PB - Springer

T2 - 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2016

Y2 - 10 October 2016 through 14 October 2016

ER -

Huisman M, Bos H, Brinkkemper S, van Deursen A, Groote JF, Lago P et al. Software that meets its Intent. In Margaria T, Steffen B, editors, Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications: 7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10-14, 2016, Proceedings, Part II. Springer. 2016. p. 609-625. (Lecture Notes in Computer Science). doi: 10.1007/978-3-319-47169-3_47

Software that meets its Intent

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this