The purpose of this chapter is to illustrate the design challenge that teams of graduate students are facing, and the solutions they devised, to develop autonomous vehicles for the worldwide speed... Show More

The purpose of this chapter is to illustrate the design challenge that teams of graduate students are facing, and the solutions they devised, to develop autonomous vehicles for the worldwide speed race competition known as The Freescale Cup. The purpose of the competition is to design the fastest car able to complete an unknown racetrack autonomously. The challenge posed by the competition is an ideal teaching ground for engineering students that can improve with a working experience the theoretical aspects learned in class in different fields such as hard-real-time system theory, control theory, model-based design theory, and computer vision theory. Besides the technical aspects, as cars are developed by teams of students, the competition is also supporting the development of soft skills (such as team work, and communication skills) that are not normally addressed by classical curricula. The results achieved after three years of participation suggest that this approach is very effective in improving the quality of engineering curricula.

Runtime verification is a technique for generating monitors from formal specification of expected behaviors for the underlying system. It can be applied to automatically evaluate system execution... Show More

Runtime verification is a technique for generating monitors from formal specification of expected behaviors for the underlying system. It can be applied to automatically evaluate system execution, either on-line or off-line, analyzing extracted execution traces; or it can be used online during operation, potentially steering the application back to a safety region if a property is violated. As a so-called light-weighted formal method, runtime verification bridges the gap between system design and implementation and shorten the distance of software quality assurance between the software testing and model checking and theorem proving. Runtime verification is considered as a highly scalable and automatic technique. Most of current runtime verification research are endeavored on the program context, in other words, on the program side and falls in the implementation level. These applications limited the benefits of runtime verification that bridges the gap among types of applications. With the proliferation of embedded systems and mobile device, dynamically verifying the firmware and mobile apps becomes a new emerging area. Due to the characteristics of runtime verification technique and limitations of the robotics systems, so far, very few research and project are located in the runtime verification on the firmware of embedded systems, which appear in most of robotics systems. Robotics systems are programmed on the firmware and only observed on device. In this paper, the authors first discussed the current runtime verifications on the embedded systems with limitations. After that, a layered runtime verification framework will be presented for the firmware verification. The case study is applied on the commonly recognized educational toolkit – LEGO Mindstorm robotics systems.

Autonomous robotics systems (ARSs) consist of multiple heterogeneous objects and intelligent inferences that are expected to take appropriate actions even in unforeseen circumstances. Dynamic... Show More

Autonomous robotics systems (ARSs) consist of multiple heterogeneous objects and intelligent inferences that are expected to take appropriate actions even in unforeseen circumstances. Dynamic reconfiguration of ARSs is a key enabling technology and plays a major role in the future cyber-enabled battle field. This research work, focused on the development of a formal approach to the specification and verification of reconfigurability of ARSs. Two typical problems w.r.t. the dynamic adaptation and reconfiguration of ARSs were identified and studied. The first problem is how to formally represent the ARSs and describe the reconfigurable behavior precisely so that the ARSs can adapt to the new changes. The second problem focuses on how to analyze and verify the formal model of the reconfiguration and ensure the correctness of the system during reconfiguration. Considering behavior preserving in the reconfiguration model, a net reconfigurations based on the natural transformation is introduced.