AbC is a process calculus designed for describing collective adaptive systems, whose distinguishing feature is the communication mechanism relying on predicates over attributes exposed by components. A novel approach to the analysis of concurrent systems modelled as AbC terms is presented that relies on the UMC model checker, a tool based on modelling concurrent systems as communicating UML-like state ma- chines. A structural translation from AbC specifications to the UMC in- ternal format is provided and used as the basis for the analysis. Three dif- ferent algorithmic solutions of the well studied stable marriage problem are described in AbC and their translations are analysed with UMC. It is shown how the proposed approach can be exploited to identify emerging properties of systems and unwanted behaviour.
Verifying properties of systems relying on attribute-based communication
Mazzanti F
2017
Abstract
AbC is a process calculus designed for describing collective adaptive systems, whose distinguishing feature is the communication mechanism relying on predicates over attributes exposed by components. A novel approach to the analysis of concurrent systems modelled as AbC terms is presented that relies on the UMC model checker, a tool based on modelling concurrent systems as communicating UML-like state ma- chines. A structural translation from AbC specifications to the UMC in- ternal format is provided and used as the basis for the analysis. Three dif- ferent algorithmic solutions of the well studied stable marriage problem are described in AbC and their translations are analysed with UMC. It is shown how the proposed approach can be exploited to identify emerging properties of systems and unwanted behaviour.File | Dimensione | Formato | |
---|---|---|---|
prod_391746-doc_151010.pdf
non disponibili
Descrizione: Verifying properties of systems relying on attribute-based communication
Tipologia:
Versione Editoriale (PDF)
Dimensione
618.42 kB
Formato
Adobe PDF
|
618.42 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
prod_391746-doc_159231.pdf
accesso aperto
Descrizione: Verifying properties of systems relying on attribute-based communication
Tipologia:
Versione Editoriale (PDF)
Dimensione
405.88 kB
Formato
Adobe PDF
|
405.88 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.