AMARETTO 2017 Abstracts

Full Papers
Full Papers
Paper Nr: 1
Title:

Combining Techniques to Verify Service-based Components
Authors:

Pascal André, Christian Attiogbé and Jean-Marie Mottu
Abstract: Early verification is essential in system development because late error detection involves a costly correction and approval process. Modelling real life systems covers three aspects of a system (structure, dynamics and functions) and one verification technique is not sufficient to check the properties related to these aspects. Considering Service-based Component Models, we propose a unifying schema called multi-level contracts that enables a combination of verification techniques (model checking, theorem proving and model testing) to cover the model V&V. This proposal is experimented using the Kmelia language and its COSTO tool.
Download
Paper Nr: 2
Title:

Concurrent History-based Usage Control Policies
Authors:

Fabio Martinelli, Ilaria Matteucci, Paolo Mori and Andrea Saracino
Abstract: The sharing of data and resources is one of the cornerstones of our society. However, this comes together with several challenges regarding the increasing need of guaranteeing security and privacy during both the access and the usage of such shared resources. Access control policies first, and usage control policies secondly, have been introduced to overcome issues related to the access and usage of resources. However, the introduction of distributed and cloud systems to share data and resources enables the concurrent and shared access to the same resources. Here we present an enhanced version of History-based Usage Control policies in which we are able to manage concurrent access and usage of resources by several subjects, whose actions may influence one another. Moreover, to ease the understanding of the proposed approach, we present a reference example where a document is shared among a set of people having different roles in a company.
Download
Paper Nr: 4
Title:

Validating TOSCA Application Topologies
Authors:

Antonio Brogi, Antonio Di Tommaso and Jacopo Soldani
Abstract: The Topology and Orchestration Specification for Cloud Applications (TOSCA) is a standardised metamodel that permits specifying cloud applications, and automating their deployment and management. TOSCA permits describing the structure of an application as a topology graph, which can then be exploited by TOSCAcompliant cloud platforms to automate the deployment of the components forming an application. In this paper we formalise the conditions that must hold for checking the validity of TOSCA application topologies, and we present an open-source prototype of validator (called SOMMELIER) that implements such conditions.
Download
Paper Nr: 7
Title:

Enhancing Models Correctness through Formal Verification: A Case Study from the Railway Domain
Authors:

Davide Basile, Felicita Di Giandomenico and Stefania Gnesi
Abstract: Model-based approaches are widely used for analysing systems belonging to a variety of domains, including the transportation sector. A critical issue with models is their validation, in order to justifiably put reliance on the analysis results they provide (including non functional indicators such as reliability, performance and energy consumption). Typically, cross-validation is performed, e.g. through exercising modelling by different formalisms/tools or through forms of experimental analysis. In this paper, we address validation of a case study from the railway domain via formal techniques, specifically with automata-based models. Validation of interaction aspects of Stochastic Activity Networks models of rail road switch heaters, developed for the purpose of evaluating energy consumption and reliability indicators, is performed through a tool based on contract automata, a recently introduced formalism for verifying properties of communication-based applications.
Download