Modeling and Analysis of Real-Time Software Based on Resource Timed Communicating Sequential Process

2011 ◽  
Vol 225-226 ◽  
pp. 802-806
Author(s):  
Yi Zhu
Keyword(s):  
Energy Consumption ◽  
Real Time ◽  
Formal Method ◽  
Optimal Path ◽  
Minimum Energy ◽  
Energy Calculation ◽  
Sequential Process ◽  
Real Time Systems ◽  
Modeling And Analysis ◽  
Time Systems

With the progress of low-power research on real-time systems, the estimation and analysis of energy consumption of real-time systems becomes a hot topic. Process Algebra is a formal method fit for analyzing the functional properties of real-time systems, but it can not analyze the energy consumption properties. This paper proposes a formal method support for modeling and analyzing energy consumption of real-time software. Resource Timed Communicating Sequential Process (RTCSP) is proposed in this paper can handle it efficiently by extending resource information on Timed Communicating Sequential Process (TCSP). In this paper, the power consumption of instructions in real-time systems is mapped into the resource of RTCSP, the energy consumption of real-time software can be modeled and optimized by using RTCSP, the optimal path algorithm is proposed to calculate the minimum energy consumption reachability path of real-time systems. This formal method improves the accuracy and efficiency of energy calculation, the calculation results can be used to quantitatively analyze and optimize the energy consumption of real-time systems.

MODELING AND ANALYSIS OF REAL-TIME SYSTEMS WITH MUTEX COMPONENTS

2012 ◽  
Vol 23 (04) ◽  
pp. 831-851 ◽  
Author(s):  
GUOQIANG LI ◽  
XIAOJUAN CAI ◽  
SHOJI YUEN
Keyword(s):  
Real Time ◽  
Timed Automata ◽  
Expressive Power ◽  
Behavioral Model ◽  
Parallel Composition ◽  
Real Time Systems ◽  
Modeling And Analysis ◽  
Compositional System ◽  
Time Systems ◽  
Timed Automaton

Timed automata are commonly recognized as a formal behavioral model for real-time systems. For compositional system design, parallel composition of timed automata as proposed by Larsen et al. [22] is useful. Although parallel composition provides a general method for system construction, in the low level behavior, components often behave sequentially by passing control via communication. This paper proposes a behavioral model, named controller automata, to combine timed automata by focusing on the control passing between components. In a controller automaton, to each state a timed automaton is assigned. A timed automaton at a state may be preempted by the control passing to another state by a global labeled transition. A controller automaton properly extends the expressive power because of the stack, but this can make the reachability problem undecidable. Given a strict partial order over states, we show that this problem can be avoided and a controller automaton can be faithfully translated into a timed automaton.

Sokrates-SA - A formal method for specifying real-time systems

1989 ◽  
Vol 27 (1-5) ◽  
pp. 513-520 ◽  
Author(s):  
Ari Okkonen ◽  
Antti Auer ◽  
Mikko Levanto ◽  
Jyrki Okkonen ◽  
Jarmo Kalaoja
Keyword(s):  
Real Time ◽  
Formal Method ◽  
Real Time Systems ◽  
Time Systems

Scheduling algorithms to reduce the static energy consumption of real-time systems

2014 ◽  
Vol 51 (2) ◽  
pp. 153-191 ◽  
Author(s):  
Vincent Legout ◽  
Mathieu Jan ◽  
Laurent Pautet
Keyword(s):  
Energy Consumption ◽  
Real Time ◽  
Scheduling Algorithms ◽  
Real Time Systems ◽  
Static Energy ◽  
Time Systems

Energy harvesting earliest deadline first scheduling algorithm for increasing lifetime of real time systems

2019 ◽  
Vol 118 (4) ◽  
pp. 160
Author(s):  
G. Madhumita ◽  
G. Rajini ◽  
B. Subisha
Keyword(s):  
Energy Consumption ◽  
Energy Harvesting ◽  
Real Time ◽  
Scheduling Algorithm ◽  
Earliest Deadline First ◽  
Real Time Systems ◽  
Tasks Scheduling ◽  
Time Systems ◽  
Earliest Deadline ◽  
Reducing Energy

In this paper, a new approach for energy minimization in energy harvesting real time systems has been investigated. Lifetime of a real time systems is depend upon its battery life.  Energy is a parameter by which the lifetime of system can be enhanced.  To work continuously and successively, energy harvesting is used as a regular source of energy. EDF (Earliest Deadline First) is a traditional real time tasks scheduling algorithm and DVS (Dynamic Voltage Scaling) is used for reducing energy consumption. In this paper, we propose an Energy Harvesting Earliest Deadline First (EH-EDF) scheduling algorithm for increasing lifetime of real time systems using DVS for reducing energy consumption and EDF for tasks scheduling with energy harvesting as regular energy supply. Our experimental results show that the proposed approach perform better to reduce energy consumption and increases the system lifetime as compared with existing approaches.  

scholarly journals Ideal and Predictable Hit Ratio for Matrix Transposition in Data Caches

Mathematics ◽  
2020 ◽  
Vol 8 (2) ◽  
pp. 184
Author(s):  
Alba Pedro-Zapater ◽  
Clemente Rodríguez ◽  
Juan Segarra ◽  
Rubén Gran Tejero ◽  
Víctor Viñals-Yúfera
Keyword(s):  
Energy Consumption ◽  
Real Time ◽  
High Performance ◽  
Negative Impact ◽  
Data Cache ◽  
Real Time Systems ◽  
Worst Case ◽  
Tile Size ◽  
Matrix Transposition ◽  
Time Systems

Matrix transposition is a fundamental operation, but it may present a very low and hardly predictable data cache hit ratio for large matrices. Safe (worst-case) hit ratio predictability is required in real-time systems. In this paper, we obtain the relations among the cache parameters that guarantee the ideal (predictable) data hit ratio assuming a Least-Recently-Used (LRU) data cache. Considering our analytical assessments, we compare a tiling matrix transposition to a cache oblivious algorithm, modified with phantom padding to improve its data hit ratio. Our results show that, with an adequate tile size, the tiling version results in an equal or better data hit ratio. We also analyze the energy consumption and execution time of matrix transposition on real hardware with pseudo-LRU (PLRU) caches. Our analytical hit/miss assessment enables the usage of a data cache for matrix transposition in real-time systems, since the number of misses in the worst case is bound. In general and high-performance computation, our analysis enables us to restrict the cache resources devoted to matrix transposition with no negative impact, in order to reduce both the energy consumption and the pollution to other computations.

FORMAL METHOD FOR AUTOMATED TRANSFORMATION OF LOTOS SPECIFICATIONS TO ESTELLE SPECIFICATIONS

2005 ◽  
Vol 15 (05) ◽  
pp. 873-891 ◽  
Author(s):  
HAZEM EL-GENDY ◽  
NABIL EL-KADHI
Keyword(s):  
Real Time ◽  
Formal Method ◽  
Conformance Testing ◽  
Control Flow ◽  
Semantic Model ◽  
Formal Description ◽  
Real Time Systems ◽  
Behavior Tree ◽  
Time Systems ◽  
Formal Description Techniques

ISO and IEC have jointly developed two Formal Description Techniques (FDTs) for specifying distributed real time systems such as computer/telecommunications protocols. These are Lotos and Estelle. In this paper, a formal method for automated transformation of a Lotos specification to an Estelle specification is presented. The method is applicable to various Lotos specification styles and to various communications protocols of ISO OSI layers. Our method has applications in conformance testing of such systems and building common semantic model for the various FDTs. In this paper, we develop an algorithm for constructing a 'Data Oriented'-Restricted Behavior Tree T that represent both the control flow aspects and the data flow aspects of the system. Then, we develop an algorithm for constructing the Estelle specifications from T. A minimization rule is also developed to optimize the size of the Estelle specification by reducing both the number of states and the number of transitions.

Sign in / Sign up

Export Citation Format

Share Document