ETD system

Electronic theses and dissertations repository

 

Tesi etd-05252016-110716


Thesis type
Tesi di dottorato di ricerca
Author
ZENZARO, SIMONE
URN
etd-05252016-110716
Title
On Modularity In Abstract State Machines
Settore scientifico disciplinare
INF/01
Corso di studi
SCIENZE DI BASE "GALILEO GALILEI"
Commissione
tutor Prof. Gervasi, Vincenzo
Parole chiave
  • Abstract State Machines
  • ASM
  • Software Engineering
  • Formal Methods
  • Formal Languages
Data inizio appello
25/06/2016;
Consultabilità
completa
Riassunto analitico
In the field of model based formal methods we investigate the Abstract State Machine (ASM) modularity features. With the growing complexity of systems and the experience gained in more than thirty years of ASM method application a need for more manageable models emerged. We mainly investigate the notion of modules in ASMs as independent interacting components and the ability to identify portions of the machine state with the aim of improving the modelling process.<br>In this thesis we provide a language level semantically well defined solution for (1) the definition of ASM modules as independent services and their communication behaviour; (2) a new construct that operates on the global state of an ASM machine that ease the management of state partitions and their identification; (3) a novel transition rule for the management of computations providing different execution strategies and putting termination condition for the machine inside the specification; (4) a data definition convention along with a new transition rule for their manipulation via pattern matching.<br>In our work we build upon CoreASM, a well-known extensible modelling framework and tool environment for ASMs. The semantic of our modularity constructs is compatible with the one defined for the CoreASM interpreter. This ease the implementation of extension plugins for tool support of modularity features.<br>A real world system use case ground model ends the thesis exemplifying the practical usage of our modularity constructs.
File