Preprints of the 30th IFAC Workshop on Real-Time Programming and 4th International Workshop on Real-Time Software

October 12–14, 2008. Wisła, Poland

30th IFAC Workshop on Real-Time Programming and 4th International Workshop on Real-Time Software

• Improving Predictability in Service Oriented Architectures
  175 Real-Time Systems, Service Oriented Architectures, Resource Management. Alejandro Alonso, Emilio Salazar, Jorge Lopez, pages 7 – 12. Show abstract facilitate communication and distributed intelligence across groups of users using different wireless standards. It efficiently supports the communication between humans and embedded systems. The target applications in the MORE project have some time requirements. However, it has not been possible to provide full support to these type of requirements. In this paper, CPU budgets are used to provide some support for meeting this type of requirements and to improve system predictability, when services with time requirements are executed.
• System Software Support for Router Fault Tolerance
  194 Router, Router Faults, Fault Tolerance, Generalized Algorithm of Fault Tolerance, Reliability Muhammad Azam, Nicholas Ioannides, Mark Rümmeli, Igor Schagaev, pages 13 – 18. Show abstract Improvements to router reliability using the generalized algorithm of fault tolerance (GAFT) are presented using time, structure and information types of redundancy. Router functionality and options to tolerate faults are discussed and analysed. Separation of toleration of malfunction and permanent faults is discussed in terms of their impact on system reliability. A scheme of reliability improvement for router is proposed using system software recovery points, with brief explanation of their implementation. Keywords : Router, Router Faults, Fault Tolerance, Generalized Algorithm of Fault Tolerance, Reliability
• An ARTEMIS Cross-Domain Embedded System Architecture and Its Instantiation for Real-Time Automotive Applications
  187 ARTEMIS, Embedded Systems, System Architecture, AUTOSAR Huber Bernhard, Roman Obermaisser, pages 19 – 26. Show abstract The GENESYS architecture is a cross-domain reference architecture for automotive, avionic, industrial control, and consumer electronic systems. Based on the blueprint of a domain-independent Multi-Processor System-on-a-Chip (MPSoC), this architecture allows to fully exploit the economics of scale (e.g., in the semiconductor industry or in tooling market) and provides solutions to key challenges of future embedded systems (e.g., composability, robustness, integrated resource management). This paper describes the relationship and compatibility between the GENESYS architecture and the AUTOSAR . By establishing AUTOSAR on top of the GENESYS architecture, we benefit from the economics of scale by achieving a larger market for embedded processors and tools, which includes beyond automotive applications also other industrial domains and consumer electronics. Furthermore, it will be explained how the GENESYS architecture enables significant technical benefits for AUTOSAR systems such as better fault isolation and temporal predictability.
• Towards Near-Realtime Identification of Extended Objects in Low-contrast Images
  47 real-time system development, image analysis, identification, extended objects Dmitry Bushenko, Rauf Sadykhov, pages 27 – 33. Show abstract At present criminalists deal with tasks of textile fibers identification. Usually this identification is done manually and takes a long time, that is why automation of this complex process is needed, with the ultimate objective to do it with near-realtime speed. As there could be various primary goals of this identification (e.g. performance, accuracy, precise shape extraction), different identification methods may be developed. This paper presents the typical primary and secondary goals of the identification and de­scribes the algorithms and methods which allow achieving these goals. As well as the positive effects of these algorithms, negative effects are presented. Pros and cons of each algorithm are discussed, and, at last, the most optimal method is proposed for the selected goals. Keywords : real-time system development, image analysis, identification, extended objects.
• Modelling and Analyzing Real-Time System Specifications using Time Stream Petri Nets
  181 Modelling, timing constraints, real-time systems, schedulability analysis, Time Stream Petri Nets, simulation, model checking, timed automata Franco Cicirelli, Angelo Furfaro, Libero Nigro, pages 35 – 42. Show abstract This paper describes an approach to modelling and analysis of real-time systems which is based on the Time Stream Petri Nets (TSPNs) formalism. The work argues that although TSPNs were originally proposed for modelling multimedia/hypermedia systems, they are well suited for expressing timing constraints in general time-dependent systems. The approach is assisted by some developed tools, based on discrete-event simulation and on model checking in terms of Uppaal timed automata, which permit temporal analysis and in particular schedulability analysis of real-time system specifications. The paper introduces the TSPN formalism and describes an implemented transformation in Uppaal. The modelling/analysis approach is demonstrated by an example. Finally, an indication of further work is given in the conclusions.
• Lab Station for Remote Measurement and Control in Teaching Real-Time Embedded Systems and Software Engineering
  202 embedded systems, real-time systems, software tools, software engineering education, robotics Carlos Daboin, Janusz Zalewski, pages 43 – 48. Show abstract This paper presents an approach to the implementation of a web-based lab station for teaching embedded systems, real-time systems, and other related courses in programs, such as software engineering, computer science or engineering, electrical engineering, mechatronics, robotics, etc. The lab involves not only data acquisition and control access to remote devices but also a capability of remote software development, uploading and debugging. The specific device used to create a lab station in this project is a remotely controlled eBox 2300 with measurement and control capabilities, running Windows Embedded 6.0. Keywords: Embedded systems, real-time systems, software tools, software engineering education, robotics, microcontrollers, FPGA.
• Some thoughts about the past and the future of the IFAC Workshops on Real-Time Programming
  203 real-time programming Peter Elzer, pages 49 – 50. Show abstract The paper presents an account of the early occurrences of the Workshop on Real-Time Programming by one of its original organizers and advocates. Some comments on current state and future of real-time programming are also given. Keywords : real-time programming, process automation, embedded systems.
• Dynamic Activity and Task Allocation Supporting UAV Teams in Surveillance Systems
  171 Task Allocation, Distributed Control, Real-Time Control, Heterogeneous Hardware, Sensor Network Edison Pignaton de Freitas, Alécio Pedro Delazari Binotto, Carlos Eduardo Pereira, André Stork, Tony Larsson, pages 51 – 58. Show abstract The use of Unmanned Aerial Vehicles is increasing in the field of area patrolling and surveillance. A great issue that emerge in designing such systems is the target workload distribution over a fleet of UAVs, which generally have different capabilities of sensing and computing power. Targets should be assigned to the most suitable UAVs in order to efficiently perform the end-user initiated missions. To perform these missions, the UAVs require powerful high-performance platforms to deal with many different algorithms that make use of massive calculations. The use of COTS hardware (e.g., GPU) presents an interesting low-cost alternative to compose the required platform. However, in order to efficiently use these heterogeneous platforms in a dynamic scenario, such as in surveillance systems, runtime reconfiguration strategies must be provided. This paper presents a dynamic approach to distribute the handling of targets among the UAVs and a heuristic method to address the efficient use of the heterogeneous hardware that equips these UAVs, with the goal to meet also mission timing requirements. Preliminary simulation results of the proposed heuristics are also provided.
• Towards Proving a Real-Time Operating System Kernel Formally Correct
  190 Real-time operating system kernel, formal correctness proof, kernel co-processor, non-pre-emptive earliest deadline first scheduling, PEARL, PVS Grzegorz Hamuda, Wolfgang Halang, pages 59 – 64. Show abstract On-going work aiming to prove the correctness of a real-time operating system kernel is described. The kernel runs on a platform providing a separate co-processor for it, and was derived by a simplifying re-design of an earlier developed one. The main design decisions taken are outlined with special regard to the scheduling policy employed. The requirements elicited during design specification were grouped by their origins. Particularly important among them is that the kernel is to support programs written in an extended version of the real-time programming language PEARL. The selection of a formal method suitable for the envisaged purpose is discussed. It is outlined how the kernel is modeled in the specification language of PVS, and how the requirements defining its correctness are formalised.
• Static Detection of Parametric Loop Bounds on C Code
  162 parametric loop bound analysis, static analysis, source code analysis Olha Honcharova, Christoph Cullmann, Florian Martin, pages 65 – 72. Show abstract Calculation of upper loop bounds is a key component for static derivation of precise WCET estimates. This paper describes a novel data-flow based analysis to calculate conservative loop bounds on the source level, where the delivered bounds are parametric with respect to variables and expressions constant within the loop. The new method is compared with two loop-bounding tools and demonstrates more precise bounds.
• Effect of Stochastic Load Dependencies on Queue Sojourn Times
  173 Stochastic Load Models, Frechet Bounds, Hoeffding Bounds, Stochastic Dependency, Scheduling Analysis, Queue Sojourn Time Analysis Matthias Ivers, Rolf Ernst, pages 73 – 78. Show abstract We discuss the applicability and consequences of probabilistic modeling for safety critical real-time systems. While deterministic task models characterize a task execution by its worst-case execution time (WCET), probabilistic models allow a better model especially for tasks with highly variable execution times by using a distribution on possible execution times. We apply a queuing sojourn time analysis of tasks with probabilistic execution times with upper and lower bounds guaranteed under any stochastic dependency. The results show how big the effect of dependencies really is and that execution time dependency is vital to the calculation of response times. We propose the use of Fréchet-bounds and probability boxes to make real-time systems with execution-time dependencies accessible to probabilistic real-time analysis.
• Hardware Testing on the Level of Tasks
  191 real-time, scheduling algorithms, fault tolerance, operating systems, diagnostic tests Thomas Kaegi-Trachsel, Igor Schagaev, Juerg Gutknecht, pages 79 – 84. Show abstract In this paper we give an introduction into fault tolerant computing and explain the generalized algorithm of fault tolerance with the several steps required to make a system fault tolerant. We show that having a hardware test assigned to every task is a powerful way to detect certain types of faults. To reduce the testing overhead and keep the system responsive, we show an algorithm that partitions the tests into the ones that are supposed to run asynchronously from the synchronous tests. Keywords : real-time, scheduling algorithms, fault tolerance, operating systems, diagnostic tests
• Co-design in Heterogeneous Wireless Networked Control Systems
  176 Networked Control System, Co-design approach, Heterogeneous networks, Quality of service, Quality of Control. Zeashan Hameed Khan, Denis Genon-Catalot, Jean Marc Thiriet, pages 85 – 90. Show abstract This paper presents a co-design approach for heterogeneous wireless networked control systems (HWNCS). An isolated design of controller and network architecture for the networked control system does not guarantee good performance if network dynamics are not included in the loop. Estimation of the delay, packet loss and errors is important especially when the control information passes through a heterogeneous wireless network. Co-design approach for the HWNCS, suggests that the control system must accommodate the variations in network quality of service or vice versa, so that it will not affect the stability and performance of the system over network.
• Adaptive Message Scheduling for a Real-Time Distributed Control System
  172 real-time control, adaptive real-time communication, Petri net, fuzzy logic scheduling, genetic algorithms, distributed control. Tiberiu Letia, Radu Miron, Mihai Hulea, pages 91 – 96. Show abstract The behavior of a real-time distributed control system is strongly influenced by the variable message delays when the communication system is highly loaded. The distributed control and information components need information from other components before some specified deadlines; otherwise their performances are seriously diminished. The changing of the transmission demands requires the adaptation of the communication system such that the software real-time requirements are fulfilled. Online fuzzy logic schedulers for ordering the messages are used for this purpose. The tuning of fuzzy membership functions parameters is performed offline by a genetic algorithm. Keywords: real-time control, adaptive real-time communication, Petri net, fuzzy logic scheduling, genetic algorithms, distributed control.
• Effect of Packet Loss on the Quality of Control of a Networked Mobile Robot
  170 Autonomous mobile robots, Networked control systems, Wireless network, Bayesian networks, Horizontal handoff, Quality of Service, Quality of Control, TrueTime simulation Amine Mechraoui, Khan Zeachan Hameed, Thiriet Jean-Marc, pages 97 – 101. Show abstract This paper describes a wireless network based control of a Khepera mobile robot moving in a WLAN distributed infrastructure. Due to the dependence of quality of control (QoC) over network quality of service (QoS), a simulation is performed for packet losses and compared to actual results in the lab environment. The network effects are examined and critical limit is determined for which control quality is acceptable. A Bayesian network approach is proposed for the decision of switching between the embedded and off-board controller as well as the horizontal handoff in multi-station scenario.
• Wireless Sensor Gateway for Industrial Networks Connection
  168 Gateway, Industrial Network, Modulation, BFSK, QPSK, QAM Zdenek Machacek, Vilem Srovnal Jr., Vilem Srovnal, pages 103 – 108. Show abstract The main objective of this paper is to show new possibilities of wireless communication for mobile industrial sensors in the real time. The network topology, signal modulations and industrial Ethernet protocol are discussed here. We have been focusing our research on real time communication of wireless sensors. Distance of sensors could be more than 30 meters and there is possibility to communication on different frequencies. The presented communication gateway is a one part of the whole wireless sensors network. The gateway provides communication by various industrial protocols common communication language. Furthermore we based our wireless communication system on 2x2 MIMO design. This solution offers significant increases in data throughput and link range without additional bandwidth or transmit power. The network communication nodes with multiple inputs and multiple outputs are designed as embedded mobile devices. With regard to real time data transfer communication, there is presented signal modulations (BFSK, QPSK, 16QAM, 64QAM) and protocol (PROFINET). The communication gateway software is implemented under QNX Neutrino RTOS and it includes PROFINET RT/IRT communication stack. Keywords : Gateway, Industrial Network, Modulation, BFSK, QPSK, QAM.
• Schedulability Analysis and Performance Evaluation of WSAN
  143 Real-time systems, Wireless sensors and actuators networks, Embedded systems, Monitoring and control in real time Diego Martínez, Patricia Balbastre, Francisco Blanes, José Simó, Alfons Crespo, pages 109 – 116. Show abstract The current trend in the development of Networked Control Systems (NCS) is the use of wireless networks to communicate the system nodes, which have been called Wireless Sensors and Actuators Networks (WSAN). This trend is principally to increase flexibility and reliability of these applications and to reduce the implementation cost. Several protocols have been used, however the latency and jitter presented in the transmission period produce that not always a similarity between experimental and simulation results can be obtained. This is because imprecise models for analyzing and designing these systems are used, and to make use of inadequate validation methods and platforms that do not support the models utilized. Therefore this paper presents a method to analyze end – to – end schedulability of WSAN, and evaluate the performance of case study using Medium Access Control (MAC) algorithms TDMA and CSMA – CA . Keywords : Real-time systems, Wireless sensors and actuators networks, Embedded systems, Real time monitoring and control .
• Impacts of Software Architectures on Cache Predictability in High-Integrity Systems
  196 System Architectures, Cache memories, Worst-case Execution Time, Timing Analysis Enrico Mezzetti, Tullio Vardanega, pages 117 – 122. Show abstract The current trend in the High Integrity Real-Time System domain steadily moves—by need if not by will—toward the adoption of processors with advanced architectural features like caches. Whilst caches have been shown to be a very effective means to speeding up memory accesses in the average case, the unpredictability of caches threatens the practicability and trustworthiness of system analysis and validation. In this paper we consider the impact that real-time software architectures may have on the cache behavior, with a view to addressing system predictability in an early stage of the software development process.
• Formal modelling framework of data acquisition software using a synchronous approach, for timing analysis
  167 Data acquisition, formal validation, embedded systems, synchronous modelling. Lionel Morel, Jean-Philippe Babau, Belgacem Ben-Hedia, pages 123 – 130. Show abstract In the field of process control, data acquisition modules (such as device drivers) require special care in their design, because they usually stand as bottlenecks between hardware devices and control applications. In particular timing constraints on occurrences of data are often given based on intuition and empirical experience. The work presented here intends to provide a formal model to characterize timing properties such as input data delay. As an illustration, a model of a simple data acquisition module is presented. We show how the formal model can be exploited to establish bounds of delay.
• Reconfigurable Network on Chip Architecture for Aerospace Applications
  192 Reliability, Fault Tolerance, Redundancy, Network on Chip (NoC), Reconfigurability,Application Specific NoC, Avionics, Aircraft Control Systems, CRAN project, ONBASS project Kasra Motamedi, Nicholas Ioannides, Mark Rümmeli, Igor Schagaev, pages 131 – 136. Show abstract A fault tolerant network on chip (FT-NoC) system with reconfigurable architecture for aerospace applications is proposed. Applying different types of redundancy on chip increases reliability, efficiency and effectiveness of the NoC and, at large, the aircraft control system itself. The central theme is the application of redundancy to tolerate hardware faults in the processor cores of the NoC system’s functional units. Second theme is the implementation of an application-specific configuration topology for the aircraft control system. The elements inside the chip are designed by considering reliability, fault tolerance and power consumption. Time, information and structural redundancies are implemented to achieve tolerance against potential permanent or transient faults. The proposed NoC system benefits aircraft control systems through higher reliability, parallelism in wire speed, reconfigurability of hardware for real time data processing, and also by lowering power consumption. Keywords : Reliability, Fault Tolerance, Redundancy, Network on Chip (NoC), Reconfigurability, Application Specific NoC, Avionics, Aircraft Control Systems, ONBASS project
• Real Time control of 20 DoF humanoid robot
  164 Real Time Control. Robotics. Real Time Operating Systems. Embedded Systems. Manuel Muñoz, J.Francisco Blanes, Miguel Albero, Javier O. Coronel, José E. Simó, Alfons Crespo, pages 137 – 142. Show abstract Robot control is a typical scenario for real time application benchmarking. Control quality many times is observed in terms of robot interaction and mobility performance. This is more obvious and complex when the robot is inherently unstable like a biped robot, where unaccomplished time requirements could trigger instability and even falls. This paper described the work performed to control 20 servomotors actuators, ensuring time accuracy and output actuator quality. The time restrictions about this are a clear case of system for which operability is decreasing when control deadlines are violated. Thus, various solutions are analyzed to implement the 20 PPM software signal generation which control the 20 joins in a biped robot. For this work an ARM7 microcontroller has been used in an embedded system that provides robot autonomy in terms of computational resources for control. Different solutions have been implemented to guarantee time restrictions performed in signal generation. This provides a correct join positioning. Finally, a RTOS based version has been implemented and developed on PaRTiKle that makes available tasks like: debug, programming, code maintenance, all this assuring time requirement compliance. Keywords : Real Time Control. Robotics. Real Time Operating Systems. Embedded Systems .
• Communication Protocols for Real-Time Systems: Time vs. Events Revisited
  174 Real-time communication, Deadlines, Event-triggered, Time-triggered, Time-shared control, Master-slave systems, CAN, Ethernet, Token-ring protocol Dirk Müller, Matthias Werner, pages 143 – 148. Show abstract The sharing of a medium for communication between nodes, forming a real network, is much more cost-effective than building a fully connected mesh. Due to the then possible collisions, special techniques have to be applied. Historically, the two main schemes to handle collisions are the time-triggered (TT) and the event-triggered (ET) approach. While the former one prevents messages from collisions by time sharing, the latter one considers collisions as events and tries to resolve them. For a long time, it has been believed that time-triggered techniques are contradicting event-triggered ones and only time-triggered approaches can provide real-time communication with hard deadlines. Both statements are not true. There are several protocols like TTCAN, TTEthernet and FlexRay combining both approaches. Well-established event-triggered protocols like CAN are capable of real-time communication to a certain degree. In this article, we provide a survey to systematize on TT and ET in the context of real-time (RT) communication systems. We discuss a wide range of approaches and try to identify relations that cross the border between TT and ET.
• Linear digital controller for high-speed dynamical system
  195 Real-time control, digital control, stability, magnetic levitation Paweł Piątek, Wojciech Grega, pages 149 – 154. Show abstract Traditionally, digital control algorithms are designed without the consideration of their real-time implementation details. Designers do not care very much about real-time, digital implementations of control algorithms, such as closed-loop execution time. The digital controller design methodology often assumes that the controller is implemented exactly, even though in reality a control law can only be realized in finite precision. Due to the finite word length effect, a controller implementation may degrade the designed closed-loop performance or even destabilize the designed stable closed-loop system, if the controller digital implementation structure is not carefully chosen. The closed-loop quality measures of the discrete finite-precision approximation of the digital controller are investigated in this paper. The magnetic levitation control example demonstrated that the proposed design procedure yields more efficient discrete controller approximation.
• On the Implementation of State-space Exploration Procedure in a Relational Database Management System
  169 Formal Specification, Temporal Logic of Actions, State exploration, Relational database systems Jaroslav Rab, Ondrej Rysavy, Miroslav Sveda, pages 155 – 160. Show abstract An examination of discrete system's behavior can be done by exhaustive exploration of the state space that is generated according to the assigned domain semantics. Model-checking is the matured discipline that allows to explore state space as large as several millions of states. In this paper, we describe a novel approach to the implementation of state exploration procedure using PL/SQL, the language of Oracle relational database system. The high efficiency of database systems when dealing with large amounts of data and relatively cheap hardware available nowadays advocates the use of relational database as an implementation platform for practical exhaustive state exploration algorithm with the hope that this platform may scale up the model checking method to hundreds of millions of explorable states.
• Integration of Automation Devices in Web Service supporting Systems
  186 SOA, fieldbus integration Matthias Riedl, Thomas Bangemann, Christian Diedrich, Robert Harrison, Daniel Wuwer, Radmehr Monfared, pages 161 – 166. Show abstract While introducing new concepts it is essential to consider the integration of components already existing or being based on alternative and well established technologies. For several reasons like investments, skills of persons, or others it is the usual case not to replace complete installations. These are extended using the same or improved technologies. Within the SOCRADES project, the integration of non web service enabled automation components is done using gateways or mediators. The integration of this kind of automation equipment also imposes requirements regarding extended configuration capabilities of the SOCRADES engineering concept. The paper presents approaches to integrate existing automation devices into upcoming Web Service based applications. To cope with a broad range of automation equipment and applications, the integration concept targets one of the world-leading industrial communication systems – PROFIBUS.
• Safe and Secure Partitioned Systems and Their Certification - Invited Paper
  207 Safety, security, safety-critical systems, Integrated Modular Avionics, certification George Romanski, pages 167 – 172. Show abstract The paper reviews some of the most important aspects of certification of real-time safety-critical systems, using the example of Integrated Modular Avionics. Security issues are also addressed where these relate to airborne systems and may be used to provide multiple independent levels of security.
• Specification Design Method for Reactive Embedded Systems - A Case Study
  206 embedded systems, software specification Benny Shimony, Ioanis Nikolaidis, Pawel Gburzynski, Eleni Stroulia, pages 173 – 180. Show abstract We report on a case study that evaluates a top-down design approach geared to the wireless sensor network (WSN) domain. Starting from a high-level specification tool based on the DisCo system, we evaluate an intermediate level of modeling based on an FSM automaton description using two types of tools and translation methods. The first is a simulation and coordination environment, and the second is a timed-automaton form with the UPPAAL tool. In both methods we incorporate model components that represent the environment, resulting in a more realistic operational estimate of the design by simulation and increasing our ability to analyze the feasibility of various design facets, i.e., real time behavior, energy use, computation, memory resources etc.
• Algorithm for Energy Optimal Routing of Periodic Messages with Real-Time Constraints in Sensor Networks.
  165 Routing algorithms, Real-time, Sensor networks, Multi-commodity network flow, Linear programming Jiri Trdlicka, Zdenek Hanzalek, pages 181 – 186. Show abstract This paper is motivated by the need of an algorithm for optimal real-time routing in multi-hop communication networks for periodically sent messages with multi-source/multi-sink connections. The optimization problem has various constraints like the capacity of each link and deadline of each communication demand. The objective is to find the optimal routing in terms of energy consumption. The algorithm is based on a minimum-cost multi-commodity network flow model. The model supposes periodically sent data with different period for each communication demand. The data can be fragmented and sent via several routing paths. The work is concluded with a routing example and with benchmark evaluation for networks with up to 144 nodes.
• Developing Self-Managing Embedded Systems with ASSL
  193 self-managing systems, embedded systems, ASSL, formal methods Emil Vassev, Mike Hinchey, pages 187 – 194. Show abstract We present a new formal approach to the implementation of embedded systems, arrived at by introducing self-management capabilities to the same. We use the ASSL (Autonomic System Specification Language) framework to approach the problem of formal specification and automatic code generation of embedded systems. Some features of ASSL help to specify event-driven embedded systems where hardware is sensed via special metrics intended to drive events and self-management policies. The latter can be specified to handle critical situations in an autonomous reactive manner. Moreover, we present a case study where we use ASSL to specify control software for the wide-angle camera carried on board by NASA’s Voyager II spacecraft.
• Safe control for systems with value- and time-dependant deviations
  184 real-time systems, technical processes, consistency, control Dieter Zoebel, Christian Weyand, Christian Schwarz, pages 195 – 200. Show abstract Real-time scheduling is both based on a broad theoretical background and available through a multitude of tools and infrastructures. The central input parameters to this discipline are the demand for execution time and the real-time conditions given as deadlines or periods. The former has attracted a lot of research efforts, mainly in the scope of worst case execution time analysis. However, the latter did not gain the same degree of attraction up to now. The derivation of real-time conditions is deeply application dependent taking into account the technical facilities as well as the specified requirements. Despite this heterogeneity a canonical process model is proposed to verify program code against specified requirements. The corresponding approach is based upon a dedicated calculus to backtrack and propagate the maximal and minimal imprecisions in time and value of the data available to the instant of executing the canonical processes.