Specification and verification of modal properties for structured systems

Andrea Vandin

doi:10.1007/978-3-642-33654-6_31

Specification and verification of modal properties for structured systems

Andrea Vandin^*

^*Corresponding author for this work

IMT Institute for Advanced Studies Lucca

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

Abstract

System specification formalisms should come with suitable property specification languages and effective verification tools. We sketch a framework for the verification of quantified temporal properties of systems with dynamically evolving structure. We consider visual specification formalisms like graph transformation systems (GTS) where program states are modelled as graphs, and the program behaviour is specified by graph transformation rules. The state space of a GTS can be represented as a graph transition system (GTrS), i.e. a transition system with states and transitions labelled, respectively, with a graph, and with a partial morphism representing the evolution of state components. Unfortunately, GTrSs are prohibitively large or infinite even for simple systems, making verification intractable and hence calling for appropriate abstraction techniques.

Original language	English
Title of host publication	Graph Transformations - 6th International Conference, ICGT 2012, Proceedings
Number of pages	3
Volume	7562 LNCS
Publication date	2012
Pages	423-425
ISBN (Print)	9783642336539
DOIs	https://doi.org/10.1007/978-3-642-33654-6_31
Publication status	Published - 2012
Externally published	Yes
Event	6th International Conference on Graph Transformations, ICGT 2012: Modeling and Analysis of Dynamic Structures - University of Bremen, Bremen, Germany Duration: 24 Sept 2012 → 29 Sept 2012 Conference number: 6

Conference

Conference	6th International Conference on Graph Transformations, ICGT 2012
Number	6
Location	University of Bremen
Country/Territory	Germany
City	Bremen
Period	24/09/2012 → 29/09/2012

Series	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	7562 LNCS
ISSN	0302-9743

Access to Document

10.1007/978-3-642-33654-6_31

OpenUrl availability

Full text

Cite this

@inproceedings{576424a627d34476bf150f970bc00130,

title = "Specification and verification of modal properties for structured systems",

abstract = "System specification formalisms should come with suitable property specification languages and effective verification tools. We sketch a framework for the verification of quantified temporal properties of systems with dynamically evolving structure. We consider visual specification formalisms like graph transformation systems (GTS) where program states are modelled as graphs, and the program behaviour is specified by graph transformation rules. The state space of a GTS can be represented as a graph transition system (GTrS), i.e. a transition system with states and transitions labelled, respectively, with a graph, and with a partial morphism representing the evolution of state components. Unfortunately, GTrSs are prohibitively large or infinite even for simple systems, making verification intractable and hence calling for appropriate abstraction techniques.",

author = "Andrea Vandin",

year = "2012",

doi = "10.1007/978-3-642-33654-6_31",

language = "English",

isbn = "9783642336539",

volume = "7562 LNCS",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "423--425",

booktitle = "Graph Transformations - 6th International Conference, ICGT 2012, Proceedings",

note = "6th International Conference on Graph Transformations, ICGT 2012 : Modeling and Analysis of Dynamic Structures, ICGT 2012 ; Conference date: 24-09-2012 Through 29-09-2012",

}

Vandin, A 2012, Specification and verification of modal properties for structured systems. in Graph Transformations - 6th International Conference, ICGT 2012, Proceedings. vol. 7562 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 7562 LNCS, pp. 423-425, 6th International Conference on Graph Transformations, ICGT 2012, Bremen, Germany, 24/09/2012. https://doi.org/10.1007/978-3-642-33654-6_31

Specification and verification of modal properties for structured systems. / Vandin, Andrea.
Graph Transformations - 6th International Conference, ICGT 2012, Proceedings. Vol. 7562 LNCS 2012. p. 423-425 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 7562 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

TY - GEN

T1 - Specification and verification of modal properties for structured systems

AU - Vandin, Andrea

N1 - Conference code: 6

PY - 2012

Y1 - 2012

N2 - System specification formalisms should come with suitable property specification languages and effective verification tools. We sketch a framework for the verification of quantified temporal properties of systems with dynamically evolving structure. We consider visual specification formalisms like graph transformation systems (GTS) where program states are modelled as graphs, and the program behaviour is specified by graph transformation rules. The state space of a GTS can be represented as a graph transition system (GTrS), i.e. a transition system with states and transitions labelled, respectively, with a graph, and with a partial morphism representing the evolution of state components. Unfortunately, GTrSs are prohibitively large or infinite even for simple systems, making verification intractable and hence calling for appropriate abstraction techniques.

AB - System specification formalisms should come with suitable property specification languages and effective verification tools. We sketch a framework for the verification of quantified temporal properties of systems with dynamically evolving structure. We consider visual specification formalisms like graph transformation systems (GTS) where program states are modelled as graphs, and the program behaviour is specified by graph transformation rules. The state space of a GTS can be represented as a graph transition system (GTrS), i.e. a transition system with states and transitions labelled, respectively, with a graph, and with a partial morphism representing the evolution of state components. Unfortunately, GTrSs are prohibitively large or infinite even for simple systems, making verification intractable and hence calling for appropriate abstraction techniques.

U2 - 10.1007/978-3-642-33654-6_31

DO - 10.1007/978-3-642-33654-6_31

M3 - Article in proceedings

AN - SCOPUS:84867648000

SN - 9783642336539

VL - 7562 LNCS

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 423

EP - 425

BT - Graph Transformations - 6th International Conference, ICGT 2012, Proceedings

T2 - 6th International Conference on Graph Transformations, ICGT 2012

Y2 - 24 September 2012 through 29 September 2012

ER -

Vandin A. Specification and verification of modal properties for structured systems. In Graph Transformations - 6th International Conference, ICGT 2012, Proceedings. Vol. 7562 LNCS. 2012. p. 423-425. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 7562 LNCS). doi: 10.1007/978-3-642-33654-6_31

Specification and verification of modal properties for structured systems

Abstract

Conference

Access to Document

OpenUrl availability

Fingerprint

Cite this