scholarly journals Model-Checking Real-Time Control Programs. Verifying LEGO Mindstorms Systems Using UPPAAL

1999 ◽  
Vol 6 (53) ◽  
Author(s):  
Torsten K. Iversen ◽  
Kåre J. Kristoffersen ◽  
Kim G. Larsen ◽  
Morten Laursen ◽  
Rune G. Madsen ◽  
...  

In this paper, we present a method for automatic verification<br />of real-time control programs running on LEGO <br />RCX bricks using the verification tool UPPAAL. The control<br />programs, consisting of a number of tasks running concurrently,<br />are automatically translated into the timed automata<br />model of UPPAAL. The fixed scheduling algorithm<br />used by the LEGO RCX processor is modeled in UPPAAL,<br />and supply of similar (sufficient) timed automata<br />models for the environment allows analysis of the overall<br />real-time system using the tools of UPPAAL. To illustrate<br />our techniques we have constructed, modeled and verified<br />a machine for sorting LEGO bricks by color.

Author(s):  
Evren Samur ◽  
Ulrich Spaelter ◽  
Lionel Flaction ◽  
Pascal Maillard ◽  
Hannes Bleuler ◽  
...  

Open source software have evolved into powerful tools for real-time control of mechatronic systems. They are of interest for academic purposes, as they promise high flexibility at low cost. In this paper, we investigate the performance of an open source control architecture based on the Linux Real-Time Application Interface (RTAI) through two applications, a haptic interface for surgery simulation and a setup for the micromachining of glass. Both applications demand a compact real-time system with sufficient precision (i.e. low jitter) for online process control and data acquisition. The real-time control has been realized on a laptop with a USB-port data acquisition card. Performance measurement results show that high quality real-time control can be performed up to 2kHz via USB communication, which is sufficient for a large range of robotic or mechatronic applications. Drawbacks like the need for considerable knowledge of Linux internals for successful installation as well as the current limitations are discussed and strategies are proposed to overcome these. Both setups are currently being used for ongoing research as well as for educational purposes.


Author(s):  
Idawaty Ahmad ◽  
Mohamad Othman ◽  
Zuriati Zulkarnain ◽  
Muhammad Fauzan Othman

Water ◽  
2020 ◽  
Vol 12 (10) ◽  
pp. 2842
Author(s):  
Mario Maiolo ◽  
Stefania Anna Palermo ◽  
Anna Chiara Brusco ◽  
Behrouz Pirouz ◽  
Michele Turco ◽  
...  

The real-time control (RTC) system is a valid and cost-effective solution for urban stormwater management. This paper aims to evaluate the beneficial effect on urban flooding risk mitigation produced by applying RTC techniques to an urban drainage network by considering different control configuration scenarios. To achieve the aim, a distributed real-time system, validated in previous studies, was considered. This approach uses a smart moveable gates system, controlled by software agents, managed by a swarm intelligence algorithm. By running the different scenarios by a customized version of the Storm Water Management Model (SWMM), the findings obtained show a redistribution of conduits filling degrees, exploiting the whole system storage capacity, with a significant reduction of node flooding and total flood volume.


Symmetry ◽  
2020 ◽  
Vol 12 (1) ◽  
pp. 172 ◽  
Author(s):  
Hoyoun Lee ◽  
Jinkyu Lee

In a real-time system, a series of jobs invoked by each task should finish its execution before its deadline, and EDF (Earliest Deadline First) is one of the most popular scheduling algorithms to meet such timing constraints of a set of given tasks. However, EDF is known to be ineffective in meeting timing constraints for non-preemptive tasks (which disallow any preemption) when the system does not know the future job release patterns of the tasks. In this paper, we develop a scheduling algorithm for a real-time system with a symmetry multiprocessor platform, which requires only limited information about the future job release patterns of a set of non-preemptive tasks, called LCEDF. We then derive its schedulability analysis that provides timing guarantees of the non-preemptive task set on a symmetry multiprocessor platform. Via simulations, we demonstrate the proposed schedulability analysis for LCEDF significantly improves the schedulability performance in meeting timing constraints of a set of non-preemptive tasks up to 20.16%, compared to vanilla non-preemptive EDF.


2018 ◽  
Vol 221 ◽  
pp. 03004
Author(s):  
H J Vermaak ◽  
L Rogers

Modern day automation systems rely on fixed programming routines to carry out their operations. If an automated flexible system is introduced onto such a production line, the complete reprogramming process required for new products needs could be automated with limited loss in production time. Therefore, instead of reprogramming each new position for the robot system the system takes over real-time control of the robot and carries out the required steps autonomously. The benefit with such a system would be that the robot would not need to be reprogrammed for every new routines but is controlled in a real-time environment to carry out new procedures based on external vision sensors. Using a real-time system could remove the need for a fixed programming environment and replace it with an automated changing programming setup. This could result in a system automatically adapting to a new product introduction through real-time machine vision processing techniques.


Sign in / Sign up

Export Citation Format

Share Document