NOVA Mobility Assistive System: Developed and Remotely Controlled with IOPT-Tools

In this paper, a Mobility Assistive System (NOVA-MAS) and a model-driven development approach are proposed to support the acquisition and analysis of data, infrastructures control, and dissemination of information along public roads. A literature review showed that the work related to mobility assistance of pedestrians in wheelchairs has a gap in ensuring their safety on road. The problem is that pedestrians in wheelchairs and scooters often do not enjoy adequate and safe lanes for their circulation on public roads, having to travel sometimes side by side with vehicles and cars moving at high speed. With NOVA-MAS, city infrastructures can obtain information regarding the environment and provide it to their users/vehicles, increasing road safety in an inclusive way, contributing to the decrease of the accidents of pedestrians in wheelchairs. NOVA-MAS not only supports information dissemination, but also data acquisition from sensors and infrastructures control, such as traffic light signs. For that, it proposed a development approach that supports the acquisition of data from the environment and its control while using a tool framework, named IOPT-Tools (Input-Output Place-Transition Tools). IOPT-Tools support controllers’ specification, validation, and implementation, with remote operation capabilities. The infrastructures’ controllers are specified through IOPT Petri net models, which are then simulated using computational tools and verified using state-space-based model-checking tools. In addition, an automatic code generator tool generates the C code, which supports the controllers’ implementation, avoiding manual codification errors. A set of prototypes were developed and tested to validate and conclude on the feasibility of the proposals.

Merging and Splitting Petri Net Models within Distributed Embedded Controller Design

Design of distributed embedded controllers can benefit from the adoption of a model-based development attitude, where Petri nets modeling can provide support for a comprehensive specification and documentation of the system together with verification capabilities and automatic deployment into implementation platforms. This chapter presents a Petri nets-based development flow based on composition and decomposition of Petri net models, using Input-Output Place-Transition Petri nets (IOPT nets) as the underlying formalism, allowing reusability of models in new situations through a net addition operation, as well as partitioning of the model into components using a net splitting operation. Distributed embedded controllers are addressed adding the concept of time domains to IOPT nets. Finally, a tool chain framework is presented supporting the whole development process, from specification to implementation, including property verification, simulation, and automatic code generation for deployment into implementation platforms (considering hardware-based implementation and VHDL coding or software-oriented implementation and C coding).

Control synthesis of a class of DEDS

A new control synthesis method suitable for a special kind of discrete event dynamic systems (DEDS) is presented in this paper. The systems to be controlled are modelled by a special class of Petri nets (PN) named state machine (SM). The class is distinctive by the fact that each PN transition has only one input place and only one output place. Bipartite directed graphs (BDG) are utilized in the control synthesis process. Namely, PN in general are (from the structure point of view) the BDG. Both the state reachability tree and the corresponding control one are developed in the straight‐line procedure starting from the given initial state and directed to the desirable terminal one as well as in the backtracking procedure starting from the terminal state and directed to the initial one. After a suitable intersection of both the straight‐lined state reachability tree and the backtracking one the state trajectories of the system are obtained. After the intersection of both the straight‐lined control reachability tree and the backtracking one the control interferences corresponding to the state trajectories are obtained.