References of "Bersani, Marcello"
     in
Bookmark and Share    
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: 167 (17 UL)
Full Text
Peer Reviewed
See detailMind the gap: Robotic Mission Planning Meets Software Engineering
Askarpour, Mehrnoosh; Menghi, Claudio UL; Belli, Gabriele et al

in Proceedings of the 8th International Conference on Formal Methods in Software Engineering (2020)

In the context of robotic software, the selection of an appropriate planner is one of the most crucial software engineering decisions. Robot planners aim at computing plans (i.e., blueprint of actions) to ... [more ▼]

In the context of robotic software, the selection of an appropriate planner is one of the most crucial software engineering decisions. Robot planners aim at computing plans (i.e., blueprint of actions) to accomplish a complex mission. While many planners have been proposed in the robotics literature, they are usually evaluated on showcase examples, making hard to understand whether they can be effectively (re)used for realising complex missions, with heterogeneous robots, and in real-world scenarios. In this paper we propose ENFORCE, a framework which allows wrapping FM-based planners into comprehensive software engineering tools, and considers complex robotic missions. ENFORCE relies on (i) realistic maps (e.g, fire escape maps) that describe the environment in which the robots are deployed; (ii) temporal logic for mission specification; and (iii) Uppaal model checker to compute plans that satisfy mission specifications. We evaluated ENFORCE by analyzing how it supports computing plans in real case scenarios, and by evaluating the generated plans in simulated and real environments. The results show that while ENFORCE is adequate for handling single-robot applications, the state explosion still represents a major barrier for reusing existing planners in multi-robot applications. [less ▲]

Detailed reference viewed: 251 (18 UL)