Synkrisis : specification and analysis of bigraphical reactive systems

Bigraphs are a meta-calculus proposed by Robin Milner as a fundamental theory and modelling formalism for structures in ubiquitous computing. Existing tool support for bigraphical reasoning focuses on research aspects of the bigraphical theory, though, hindering their adoption of engineering applications. Research approaches adopt different modelling conceptions and specification formats: concrete support throughout the design process is missing, something which hinders interoperability and thus development of sophisticated toolchains for systematic model-based engineering. We propose Synkrisis, a development environment and toolchain sporting a modular approach streamlining support for bigraphical reasoning. Synkrisis supports specification and analysis where probabilistic model checking and ω-automata operations are provided through interfacing external tools.

I bigrafi sono una forma di meta-calcolo proposta da Robin Milner come teoria fondamentale e insieme formalismo per modellare entità nell'ubiquitous computing. Gli strumenti di supporto per il ragionamento automatico basati su bigrafi si sono finora concentrati sugli aspetti più teorici della teoria dei bigrafi, rendendo difficile l'adozione di questo formalismo per applicazioni ingegneristiche. Gli approcci di ricerca adottano un gran numero di modellizzazioni e formati di specifica: manca un supporto concreto lungo il processo di design, e questo finisce con il rallentare l'interoperabilità e lo sviluppo di toolchain complesse per approcci sistematici e ingegneristici basati su modelli. Proponiamo Synkrisis, ambiente di sviluppo e toolchain modulare, il cui obiettivo è di uniformare il supporto per il model checking basato sui bigrafi. Synkrisis fornisce una funzionalità di specifica e di analisi in cui il model checking probabilistico e le operazioni su ω-automi sono fornite interfacciando strumenti esterni.