2015
Contribution to book
Restricted
Safe adaptation through implicit effect coercion
Basile D, Galletta L, Mezzetti G
Context-Oriented programming languages provide us with primitive constructs to adapt programs behaviour depending on the evolution of their operational environment. In this paradigm developers must provide behaviour for any context a program may find in. A missing behaviour causes a new kind of runtime error: an adaptation error. We propose a novel mechanism, based on implicit function, that allows the execution environment to supply such behaviour when the program is not able to adapt. We assess our proposal extending a core functional language designed for adaptivity. We integrate the mechanism in a type and effect system, in the form of implicit coercions, showing that our type discipline guarantees that no adaptation errors occur.DOI: 10.1007/978-3-319-25527-9_10
Metrics:
Basile D, Galletta L, Mezzetti G
Context-Oriented programming languages provide us with primitive constructs to adapt programs behaviour depending on the evolution of their operational environment. In this paradigm developers must provide behaviour for any context a program may find in. A missing behaviour causes a new kind of runtime error: an adaptation error. We propose a novel mechanism, based on implicit function, that allows the execution environment to supply such behaviour when the program is not able to adapt. We assess our proposal extending a core functional language designed for adaptivity. We integrate the mechanism in a type and effect system, in the form of implicit coercions, showing that our type discipline guarantees that no adaptation errors occur.DOI: 10.1007/978-3-319-25527-9_10
Metrics:
See at:
doi.org 
| CNR IRIS | CNR IRIS | link.springer.com
2016
Conference article
Open Access
Playing with our CAT and communication-centric applications
Basile D, Degano P, Ferrari Gl, Tuosto E
We describe CAT, a toolkit supporting the analysis of communication-centric applications, i.e., applications consisting of ensembles of interacting services. Services are modelled in CAT as contract automata and communication safety is defined in terms of agreement properties. With the help of a simple (albeit non trivial) example, we demonstrate how CAT can (i) verify agreement properties, (ii) synthesise an orchestrator enforcing communication safety, (iii) detect misbehaving services, and (iv) check when the services form a choreography. The use of mixed-integer linear programming is a distinguished characteristic of CAT that allows us to verify context-sensitive properties of agreement.DOI: 10.1007/978-3-319-39570-8_5
Metrics:
Basile D, Degano P, Ferrari Gl, Tuosto E
We describe CAT, a toolkit supporting the analysis of communication-centric applications, i.e., applications consisting of ensembles of interacting services. Services are modelled in CAT as contract automata and communication safety is defined in terms of agreement properties. With the help of a simple (albeit non trivial) example, we demonstrate how CAT can (i) verify agreement properties, (ii) synthesise an orchestrator enforcing communication safety, (iii) detect misbehaving services, and (iv) check when the services form a choreography. The use of mixed-integer linear programming is a distinguished characteristic of CAT that allows us to verify context-sensitive properties of agreement.DOI: 10.1007/978-3-319-39570-8_5
Metrics:
See at:
hal.inria.fr 
| CNR IRIS | link.springer.com | ISTI Repository | doi.org | Hyper Article en Ligne | CNR IRIS | CNR IRIS
2016
Journal article
Open Access
Automata for specifying and orchestrating service contracts
Basile D, Degano P, Ferrari G
An approach to the formal description of service contracts is presented in terms of automata. We focus on the basic property of guaranteeing that in the multi-party composition of principals each of them gets his requests satisfied, so that the overall composition reaches its goal. Depending on whether requests are satisfied synchronously or asynchronously, we construct an orchestrator that at static time either yields composed services enjoying the required properties or detects the principals responsible for possible violations. To do that in the asynchronous case we resort to Linear Programming techniques. We also relate our automata with two logically based methods for specifying contracts.Source: LOGICAL METHODS IN COMPUTER SCIENCE, vol. 12 (issue 4)
DOI: 10.2168/lmcs-12(4:6)2016
Metrics:
Basile D, Degano P, Ferrari G
An approach to the formal description of service contracts is presented in terms of automata. We focus on the basic property of guaranteeing that in the multi-party composition of principals each of them gets his requests satisfied, so that the overall composition reaches its goal. Depending on whether requests are satisfied synchronously or asynchronously, we construct an orchestrator that at static time either yields composed services enjoying the required properties or detects the principals responsible for possible violations. To do that in the asynchronous case we resort to Linear Programming techniques. We also relate our automata with two logically based methods for specifying contracts.Source: LOGICAL METHODS IN COMPUTER SCIENCE, vol. 12 (issue 4)
DOI: 10.2168/lmcs-12(4:6)2016
Metrics:
See at:
Logical Methods in Computer Science | Logical Methods in Computer Science | CNR IRIS | CNR IRIS | lmcs.episciences.org
2016
Journal article
Open Access
Relating two automata-based models of orchestration and choreography
Basile D, Degano P, Ferrari G, Tuosto E
We investigate the relations between two automata-based models for describing and studying distributed services, called contract automata and communicating machines. In the first model, distributed services are abstracted away as automata - oblivious of their partners - that coordinate with each other through an orchestrator. The second one is concerned with the interactions occurring between distributed services, that are represented by channel-based asynchronous communications; then services are coordinated through choreography. We define a notion of strong agreement on contract automata; exhibit a natural mapping from this model to communicating machines with a synchronous semantics; and give conditions to ensure that strong agreement corresponds to well-formed choreography. Then these results are extended to a more liberal notion of agreement and to a fully asynchronous semantics of communicating machines.Source: THE JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING, vol. 85 (issue 3), pp. 425-446
DOI: 10.1016/j.jlamp.2015.09.011
Project(s): MEALS
Metrics:
Basile D, Degano P, Ferrari G, Tuosto E
We investigate the relations between two automata-based models for describing and studying distributed services, called contract automata and communicating machines. In the first model, distributed services are abstracted away as automata - oblivious of their partners - that coordinate with each other through an orchestrator. The second one is concerned with the interactions occurring between distributed services, that are represented by channel-based asynchronous communications; then services are coordinated through choreography. We define a notion of strong agreement on contract automata; exhibit a natural mapping from this model to communicating machines with a synchronous semantics; and give conditions to ensure that strong agreement corresponds to well-formed choreography. Then these results are extended to a more liberal notion of agreement and to a fully asynchronous semantics of communicating machines.Source: THE JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING, vol. 85 (issue 3), pp. 425-446
DOI: 10.1016/j.jlamp.2015.09.011
Project(s): MEALS
Metrics:
See at:
Journal of Logical and Algebraic Methods in Programming | Flore (Florence Research Repository) | CNR IRIS | CNR IRIS
2019
Journal article
Open Access
Applying supervisory control synthesis to priced featured automata and energy problems
Basile D
Software Product Line Engineering (SPLE) promotes extensive reuse of common aspects in developing new software components. Supervisory Control Theory (SCT) is a methodology to automatically synthesise a controller enforcing given safety requirements. The interplay between SPLE and SCT has recently received attention in the research community. This paper formally tackles the problem of synthesising a most permissive controller (mpc) enforcing a given requirement for a software product line (SPL). Generally, the number of products of an SPL can be exponential in the number of features, and an mpc should be synthesised for every product. To overcome this problem, the product line structure is exploited to synthesise, in the best case, a number of controllers that are linear in the number of features of the SPL. The SPL is formalised as a (Priced) Featured Automaton ((P)FA), whilst the mpc synthesis is formalised by modelling both the plant and the requirement as Extended Finite-state Automata (EFA), where quantitative aspects can be seamlessly integrated. The contributions are: (i) a formal mapping from FA to EFA; (ii) a mapping of energy problems onto synthesis of EFA; (iii) three-valued logic and partial-order reduction are used to greatly reduce the number of mpcs required. Contribution (iii) holds for a wide range of other objectives, not only energy problems. Both EFA and PFA are endowed with tools implementing algorithms that have been studied for more than a decade and both are adopted in industry. These results pave the way to reuse algorithms and tools that have been separately developed in SPLE and SCT research areas.Source: INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER (PRINT), vol. 21 (issue 6), pp. 679-689
DOI: 10.1007/s10009-019-00533-3
Metrics:
Basile D
Software Product Line Engineering (SPLE) promotes extensive reuse of common aspects in developing new software components. Supervisory Control Theory (SCT) is a methodology to automatically synthesise a controller enforcing given safety requirements. The interplay between SPLE and SCT has recently received attention in the research community. This paper formally tackles the problem of synthesising a most permissive controller (mpc) enforcing a given requirement for a software product line (SPL). Generally, the number of products of an SPL can be exponential in the number of features, and an mpc should be synthesised for every product. To overcome this problem, the product line structure is exploited to synthesise, in the best case, a number of controllers that are linear in the number of features of the SPL. The SPL is formalised as a (Priced) Featured Automaton ((P)FA), whilst the mpc synthesis is formalised by modelling both the plant and the requirement as Extended Finite-state Automata (EFA), where quantitative aspects can be seamlessly integrated. The contributions are: (i) a formal mapping from FA to EFA; (ii) a mapping of energy problems onto synthesis of EFA; (iii) three-valued logic and partial-order reduction are used to greatly reduce the number of mpcs required. Contribution (iii) holds for a wide range of other objectives, not only energy problems. Both EFA and PFA are endowed with tools implementing algorithms that have been studied for more than a decade and both are adopted in industry. These results pave the way to reuse algorithms and tools that have been separately developed in SPLE and SCT research areas.Source: INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER (PRINT), vol. 21 (issue 6), pp. 679-689
DOI: 10.1007/s10009-019-00533-3
Metrics:
See at:
CNR IRIS | link.springer.com | ISTI Repository | International Journal on Software Tools for Technology Transfer | CNR IRIS | CNR IRIS
2021
Journal article
Open Access
Analysing an autonomous tramway positioning system with the Uppaal Statistical Model Checker
Basile D, Fantechi A, Rucher L, Mandò€ G
The substitution of traditional occupancy detecting sensors with anAutonomous Positioning System (APS) is a promising solution tocontain costs and improve performance of current tramway signallingsystems. APS is an onboard system using satellite positioning andother inertial platforms to autonomously estimate the position ofthe tram with the needed levels of uncertainty and protection.However, autonomous positioning introduces, even in absence offaults, a quantitative uncertainty with respect to traditionalsensors. This paper investigates this issue in the context of anindustrial project: a model of the envisaged solution is proposed,and it is analysed using Uppaal Statistical Model Checker.A novel model-driven hazard analysis approach to the exploration ofemerging hazards is proposed. The analysis emphasises how thevirtualisation of legacy track circuits and on-board satellitepositioning equipment may give rise to new hazards, not present inthe traditional system.Source: FORMAL ASPECTS OF COMPUTING
DOI: 10.1007/s00165-021-00556-1
Metrics:
Basile D, Fantechi A, Rucher L, Mandò€ G
The substitution of traditional occupancy detecting sensors with anAutonomous Positioning System (APS) is a promising solution tocontain costs and improve performance of current tramway signallingsystems. APS is an onboard system using satellite positioning andother inertial platforms to autonomously estimate the position ofthe tram with the needed levels of uncertainty and protection.However, autonomous positioning introduces, even in absence offaults, a quantitative uncertainty with respect to traditionalsensors. This paper investigates this issue in the context of anindustrial project: a model of the envisaged solution is proposed,and it is analysed using Uppaal Statistical Model Checker.A novel model-driven hazard analysis approach to the exploration ofemerging hazards is proposed. The analysis emphasises how thevirtualisation of legacy track circuits and on-board satellitepositioning equipment may give rise to new hazards, not present inthe traditional system.Source: FORMAL ASPECTS OF COMPUTING
DOI: 10.1007/s00165-021-00556-1
Metrics:
See at:
CNR IRIS | link.springer.com | ISTI Repository | CNR IRIS | CNR IRIS
2021
Journal article
Open Access
Secure multi-party computation with service contract automata
Basile D
By combining research from model-based software engineering, dependable computing, and formal methods, it is possible to create a contract-based design methodology to enforce security accountability and reputation of distributed digital entities provided by potentially mutually distrusted organisations.Source: ERCIM NEWS, vol. 2021 (issue 126), pp. 32-33
Project(s): 4SECURAIL
Basile D
By combining research from model-based software engineering, dependable computing, and formal methods, it is possible to create a contract-based design methodology to enforce security accountability and reputation of distributed digital entities provided by potentially mutually distrusted organisations.Source: ERCIM NEWS, vol. 2021 (issue 126), pp. 32-33
Project(s): 4SECURAIL
See at:
ercim-news.ercim.eu | CNR IRIS | ISTI Repository | ISTI Repository | CNR IRIS | CNR IRIS
2021
Software
Open Access
Contract automata library
Basile D
The Contract Automata Tool is an ongoing basic research activity about implementing and experimenting with new developments in the theoretical framework of contract automata.
Basile D
The Contract Automata Tool is an ongoing basic research activity about implementing and experimenting with new developments in the theoretical framework of contract automata.
See at:
github.com | CNR IRIS | CNR IRIS
2021
Software
Open Access
Contract automata application
Basile D
This is a GUI application of the Contract Automata Toolkit, exploiting the contract automata library to put contract automata at work
Basile D
This is a GUI application of the Contract Automata Toolkit, exploiting the contract automata library to put contract automata at work
See at:
github.com | CNR IRIS | CNR IRIS
2020
Other
Metadata Only Access
4SECURail video presentation of Sparx EA and demonstrator of formal methods
Basile D
The formal methods demonstrator of Deliverable 2.2 comprises also a video presentation of the tools and artifacts developed during the project, this is the Sparx EA video.Project(s): 4SECURAIL
Basile D
The formal methods demonstrator of Deliverable 2.2 comprises also a video presentation of the tools and artifacts developed during the project, this is the Sparx EA video.Project(s): 4SECURAIL
See at:
CNR IRIS | zenodo.org
2020
Software
Open Access
4SECURail D 2.2: Sparx EA artifacts and technical documentation
Basile D
This is the model, generated source code, exported xmi model, and technical report of the Communication Supervision Layer of the UNISIG Subset 98 developed with Sparx Enterprise Architect for the Deliverable 2.2 of the 4SECURail projectProject(s): 4SECURAIL
Basile D
This is the model, generated source code, exported xmi model, and technical report of the Communication Supervision Layer of the UNISIG Subset 98 developed with Sparx Enterprise Architect for the Deliverable 2.2 of the 4SECURail projectProject(s): 4SECURAIL
See at:
CNR IRIS | zenodo.org | CNR IRIS | CNR IRIS | CNR IRIS
2017
Software
Open Access
AMPL model for the dependable dynamic vehicle routing problem
Basile D
AMPL integer linear programming program for the dependable dynamic vehicle routing problem, referred in the paper published at RSSRail 2017
Basile D
AMPL integer linear programming program for the dependable dynamic vehicle routing problem, referred in the paper published at RSSRail 2017
See at:
github.com | CNR IRIS | CNR IRIS
2016
Software
Open Access
The Stochastic Activity Network models of the rail road switch heating system for Moebius tool
Basile D
The SAN models of the rail road switch heating system This is a SAN model done in Moebius in 2015 and published at JRTPM2016 https://doi.org/10.1016/j.jrtpm.2016.03.003
Basile D
The SAN models of the rail road switch heating system This is a SAN model done in Moebius in 2015 and published at JRTPM2016 https://doi.org/10.1016/j.jrtpm.2016.03.003
See at:
github.com | CNR IRIS | CNR IRIS
2019
Software
Restricted
The Uppaal SMC model and experiments published at RSSRail 2019
Basile D
The Uppaal SMC model and experiments published at RSSRail 2019 https://link.springer.com/chapter/10.1007%2F978-3-030-18744-6_3
Basile D
The Uppaal SMC model and experiments published at RSSRail 2019 https://link.springer.com/chapter/10.1007%2F978-3-030-18744-6_3
2016
Software
Open Access
AMPL model for Weak Agreement in contract automata, implementation of weak liability checking, published at FORTE2016
Basile D
AMPL model for Weak Agreement in contract automata, implementation of weak liability checking, published at FORTE2016. This is a prototype implementation of the verification techniques for the properties of weak agreement and weak safety of a CA. The linear problems are specified using AMPL. (http://www.ampl.com/DOWNLOADS/) The main files are: weakagreement.mod weaksafety.mod To run an example print from command line "ampl flow.run", the script flow.run will be executed, that will check if the CA described in the file "flow.dat" admits weak agreement. To check weak safety it suffices to change in the file "flow.run" the model to weaksafety.mod. The specification of the CA is given in the file flow.dat. An automa is defined through: the number of nodes (it is assumed that the node 1 is the initial node); the id of the final node (assuming only one final state); the cardinality of the alphabet of actions the matrix of transitions (0 if there is no transition for the arc (n,m) 1 if there is a transition for the arc (n,m) ) for each action a matrix of labels ( 1 if the action is an offer in the transition (n,m) -1 if the action is a request in the transition (n,m) 0 if the action is a match )
Basile D
AMPL model for Weak Agreement in contract automata, implementation of weak liability checking, published at FORTE2016. This is a prototype implementation of the verification techniques for the properties of weak agreement and weak safety of a CA. The linear problems are specified using AMPL. (http://www.ampl.com/DOWNLOADS/) The main files are: weakagreement.mod weaksafety.mod To run an example print from command line "ampl flow.run", the script flow.run will be executed, that will check if the CA described in the file "flow.dat" admits weak agreement. To check weak safety it suffices to change in the file "flow.run" the model to weaksafety.mod. The specification of the CA is given in the file flow.dat. An automa is defined through: the number of nodes (it is assumed that the node 1 is the initial node); the id of the final node (assuming only one final state); the cardinality of the alphabet of actions the matrix of transitions (0 if there is no transition for the arc (n,m) 1 if there is a transition for the arc (n,m) ) for each action a matrix of labels ( 1 if the action is an offer in the transition (n,m) -1 if the action is a request in the transition (n,m) 0 if the action is a match )
See at:
github.com | CNR IRIS | CNR IRIS
2021
Software
Open Access
Uppaal models and experiments for the paper: "Formal Analysis of the UNISIG Safety Application Intermediate Sublayer." (FMICS2021)
Basile D, Rosadi I
Uppaal models of the paper Formal Analysis of the UNISIG Safety Application Intermediate Sublayer. FMICS2021 Basile, D., Fantechi, A. and Rosadi, I., 2021, August. Formal Analysis of the UNISIG Safety Application Intermediate Sub-layer. In International Conference on Formal Methods for Industrial Critical Systems (pp. 174-190). Springer, Cham. Video presentation: https://youtu.be/nGHfXi1vvg4 Mapping between the formulas described in the paper and the models ?4, ?5, ?7, ?9, ?11, ?13, ?17, ?18, ?19, ?20 -> modelConfStandard ?1, ?2, ?3, ?6, ?8, ?10, ?12, ?16 -> modelFastVerification ?14 -> modelLowerMaxLostMsgFastVerification ?15 -> modelLowerMaxLostMsg ?16' -> modelNoTransmissionDelayThreat ?21 -> modelLowerSNMax
Basile D, Rosadi I
Uppaal models of the paper Formal Analysis of the UNISIG Safety Application Intermediate Sublayer. FMICS2021 Basile, D., Fantechi, A. and Rosadi, I., 2021, August. Formal Analysis of the UNISIG Safety Application Intermediate Sub-layer. In International Conference on Formal Methods for Industrial Critical Systems (pp. 174-190). Springer, Cham. Video presentation: https://youtu.be/nGHfXi1vvg4 Mapping between the formulas described in the paper and the models ?4, ?5, ?7, ?9, ?11, ?13, ?17, ?18, ?19, ?20 -> modelConfStandard ?1, ?2, ?3, ?6, ?8, ?10, ?12, ?16 -> modelFastVerification ?14 -> modelLowerMaxLostMsgFastVerification ?15 -> modelLowerMaxLostMsg ?16' -> modelNoTransmissionDelayThreat ?21 -> modelLowerSNMax
See at:
github.com | CNR IRIS | CNR IRIS
2021
Software
Open Access
Models and experiments logs for the article published at "Formal Aspects of Computing 2021"
Basile D
EXPERIMENTS REPRODUCTION PACKAGE This repository contains the models and experiments logs for the article published at Formal Aspects of Computing https://doi.org/10.1007/s00165-021-00556-1 The model.xml contains the model, where all parameters for the set-ups are global, and comments on the queries of the verifier are available to improve readability. Since these comments are not readable by the command-line verifier, the set-up for experiments are in separate files, whose name indicate the specific set-up, among those used in the article, and the indication that these files have been used for the verifyta.exe command-line verifier of Uppaal. In all these set-ups the model is unchanged, but only the specific used parameters. The experiments for the mitigated model, third setup, are also reported in a separate file. In this case, the model has been amended as described in the article. All logs of the execution of experiments are reported. Note that in such logs the probability uncertainty (epsilon) is, in some specific case, different from the one used in the article. We also archived the executable of the used verifier for reproducibility of the logs. A legacy file "model with occ and mitigation.xml" is stored, not useful for reproducibility.
Basile D
EXPERIMENTS REPRODUCTION PACKAGE This repository contains the models and experiments logs for the article published at Formal Aspects of Computing https://doi.org/10.1007/s00165-021-00556-1 The model.xml contains the model, where all parameters for the set-ups are global, and comments on the queries of the verifier are available to improve readability. Since these comments are not readable by the command-line verifier, the set-up for experiments are in separate files, whose name indicate the specific set-up, among those used in the article, and the indication that these files have been used for the verifyta.exe command-line verifier of Uppaal. In all these set-ups the model is unchanged, but only the specific used parameters. The experiments for the mitigated model, third setup, are also reported in a separate file. In this case, the model has been amended as described in the article. All logs of the execution of experiments are reported. Note that in such logs the probability uncertainty (epsilon) is, in some specific case, different from the one used in the article. We also archived the executable of the used verifier for reproducibility of the logs. A legacy file "model with occ and mitigation.xml" is stored, not useful for reproducibility.
See at:
github.com | CNR IRIS | CNR IRIS
2020
Software
Open Access
Stratego formal models and experiments for the paper published at FORTE2020
Basile D
This is the Uppaal Stratego model published at FORTE2020 https://link.springer.com/chapter/10.1007%2F978-3-030-50086-3_1
Basile D
This is the Uppaal Stratego model published at FORTE2020 https://link.springer.com/chapter/10.1007%2F978-3-030-50086-3_1
See at:
github.com | CNR IRIS | CNR IRIS
2019
Software
Open Access
The Uppaal SMC models developed for the ASTRail project and experiments, published at Isola2018 and FMICS2019
Basile D
This repository contains various models of the ERTMS ETCS L3 Moving Block specification (https://en.wikipedia.org/wiki/European_Train_Control_System#Level_3), with increasing level of details, that stem from the ASTRail project (http://www.astrail.eu/) and the Deliverable 5.1 of X2Rail1 project (https://projects.shift2rail.org/X2RAIL-1), created with Uppaal SMC version 4.1.19 and 4.1.24 (http://www.uppaal.org/). The models and analyses have been published in Isola2018 and FMICS2019.Project(s): ASTRail
Basile D
This repository contains various models of the ERTMS ETCS L3 Moving Block specification (https://en.wikipedia.org/wiki/European_Train_Control_System#Level_3), with increasing level of details, that stem from the ASTRail project (http://www.astrail.eu/) and the Deliverable 5.1 of X2Rail1 project (https://projects.shift2rail.org/X2RAIL-1), created with Uppaal SMC version 4.1.19 and 4.1.24 (http://www.uppaal.org/). The models and analyses have been published in Isola2018 and FMICS2019.Project(s): ASTRail
See at:
github.com | CNR IRIS | CNR IRIS
2021
Software
Open Access
Publicity chair tools
Basile D
This Java app has been developed and used as part of the Publicity Chair role for the Vamos 2022 conference, https://vamos2022.isti.cnr.it/. The application connects through biblioproxy to download a series of publications, identified by their doi, and then processes the pdfs to extract the emails of authors. It is useful to create the list of participants of the last editions of specific conferences, useful for publicity chair purposes.
Basile D
This Java app has been developed and used as part of the Publicity Chair role for the Vamos 2022 conference, https://vamos2022.isti.cnr.it/. The application connects through biblioproxy to download a series of publications, identified by their doi, and then processes the pdfs to extract the emails of authors. It is useful to create the list of participants of the last editions of specific conferences, useful for publicity chair purposes.