References of "Rossi, Matteo"
     in
Bookmark and Share    
Full Text
Peer Reviewed
See detailRoboMAX: Robotic Mission Adaptation eXemplars
Askarpour, Mehrnoosh; Tsigkanos, Christos; Menghi, Claudio UL et al

in Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS) - Artifact Track (2021)

Emerging and future applications of robotic systems pose unique self-adaptation challenges. To support the research needed to address these challenges, we provide an extensible repository of robotic ... [more ▼]

Emerging and future applications of robotic systems pose unique self-adaptation challenges. To support the research needed to address these challenges, we provide an extensible repository of robotic mission adaptation exemplars. Co-designed with robotic application stakeholders including researchers, developers, operators, and end-users, our repository captures key sources of uncertainty, adaptation concerns, and other distinguishing characteristics of such applications. An online form enables external parties to supply new exemplars for curation and inclusion into the repository. We envisage that our RoboMAX repository will enable the development, evaluation, and comparison of much-needed self-adaptation approaches for the robotic systems domain. [less ▲]

Detailed reference viewed: 184 (22 UL)
Full Text
Peer Reviewed
See detailModel Checking MITL formulae on Timed Automata: a Logic-Based Approach
Menghi, Claudio UL; Bersani, Marcello; Rossi, Matteo et al

in ACM Transactions on Computational Logic (2020), 21(3),

Timed Automata (TA) is de facto a standard modelling formalism to represent systems when the interest is the analysis of their behaviour as time progresses. This modelling formalism is mostly used for ... [more ▼]

Timed Automata (TA) is de facto a standard modelling formalism to represent systems when the interest is the analysis of their behaviour as time progresses. This modelling formalism is mostly used for checking whether the behaviours of a system satisfy a set of properties of interest. Even if efficient model-checkers for Timed Automata exist, these tools are not easily configurable. First, they are not designed to easily allow adding new Timed Automata constructs, such as new synchronization mechanisms or communication procedures, but they assume a fixed set of Timed Automata constructs. Second, they usually do not support the Metric Interval Temporal Logic (MITL) and rely on a precise semantics for the logic in which the property of interest is specified which cannot be easily modified and customized. Finally, they do not easily allow using different solvers that may speed up verification in different contexts. This paper presents a novel technique to perform model checking of Metric Interval Temporal Logic (MITL) properties on TA. The technique relies on the translation of both the TA and the MITL formula into an intermediate Constraint LTL over clocks (CLTLoc) formula which is verified through an available decision procedure. The technique is flexible since the intermediate logic allows the encoding of new semantics as well as new TA constructs, by just adding new CLTLoc formulae. Furthermore, our technique is not bound to a specific solver as the intermediate CLTLoc formula can be verified using different procedures. [less ▲]

Detailed reference viewed: 139 (17 UL)
Full Text
Peer Reviewed
See detailPuRSUE -from specification of robotic environments to synthesis of controllers
Bersani, Marcello M.; Soldo, Matteo; Menghi, Claudio UL et al

in Formal Aspects of Computing (2020)

Detailed reference viewed: 158 (3 UL)