scholarly journals Exact acceleration of complex real-time model checking based on overlapping cycle

2020 ◽  
Vol 6 ◽  
pp. e272
Author(s):  
Guoqing Wang ◽  
Lei Zhuang ◽  
Yu Song ◽  
Mengyang He ◽  
Ding Ma ◽  
...  
Keyword(s):  
Real Time ◽  
Large Scale ◽  
Timed Automata ◽  
System Model ◽  
Real Time Systems ◽  
Time Model ◽  
Real Time System ◽  
Acceleration Method ◽  
Time Systems ◽  
Timed Automaton

When real-time systems are modeled as timed automata, different time scales may lead to substantial fragmentation of the symbolic state space. Exact acceleration solves the fragmentation problem without changing system reachability. The relatively mature technology of exact acceleration has been used with an appended cycle or a parking cycle, which can be applied to the calculation of a single acceleratable cycle model. Using these two technologies to develop a complex real-time model requires additional states and consumes a large amount of time cost, thereby influencing acceleration efficiency. In this paper, a complex real-time exact acceleration method based on an overlapping cycle is proposed, which is an application scenario extension of the parking-cycle technique. By comprehensively analyzing the accelerating impacts of multiple acceleratable cycles, it is only necessary to add a single overlapping period with a fixed length without relying on the windows of acceleratable cycles. Experimental results show that the proposed timed automaton model is simple and effectively decreases the time costs of exact acceleration. For the complex real-time system model, the method based on an overlapping cycle can accelerate the large scale and concurrent states which cannot be solved by the original exact acceleration theory.

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.

scholarly journals A Time Refinement Framework Based on iUML-B State Machine

2021 ◽  
Vol 2021 ◽  
pp. 1-21
Author(s):  
Han Peng ◽  
Xiaoli Zhang ◽  
Guozhen Cao ◽  
Zhouzhou Liu ◽  
Yuejuan Jing ◽  
...  
Keyword(s):  
Real Time ◽  
Timed Automata ◽  
System Modeling ◽  
Research Work ◽  
Time Constraints ◽  
Formal Modeling ◽  
Time System ◽  
Time Model ◽  
Real Time System ◽  
Time Systems

Event-B is a formal modeling language that is very suitable for software engineering, but it lacks the ability of modeling time. Researchers have proposed some methods for modeling time constraints in Event-B. The limitations with existing methods are that, first of all, the existing research work lacks a systematic time refinement framework based on Event-B; secondly, the existing methods only model time in the Event-B framework and cannot be smoothly converted to automata-based models such as timed automata that facilitate the verification of time properties. These limitations make it more difficult to model and verify real-time systems with Event-B because it is very time-consuming to prove time properties in the Event-B framework. In this paper, we firstly proposed a systematic time refinement framework to express and refine time constraints in Event-B. Secondly, we also proposed various vertical refinement patterns and horizontal extension patterns to guide modelers to refine the Event-B real-time model step by step. Finally, we use a real-time system case to demonstrate the practicality of our method. The experimental results show that the proposed method can make the real-time system modeling in Event-B more convenient and the models are easier to convert to the timed automata model, thereby facilitating the verification of various time properties.

Randomized Work Stealing for Large Scale Soft Real-Time Systems

2016 ◽  
Author(s):  
Jing Li ◽  
Son Dinh ◽  
Kevin Kieselbach ◽  
Kunal Agrawal ◽  
Christopher Gill ◽  
...  
Keyword(s):  
Real Time ◽  
Large Scale ◽  
Real Time Systems ◽  
Work Stealing ◽  
Time Systems

scholarly journals Online On-the-Fly Testing of Real-time Systems

2003 ◽  
Vol 10 (49) ◽  
Author(s):  
Marius Mikucionis ◽  
Kim G. Larsen ◽  
Brian Nielsen
Keyword(s):  
Real Time ◽  
Test Generation ◽  
Timed Automata ◽  
Online Testing ◽  
Real Time Systems ◽  
Model Checker ◽  
Test Specification ◽  
And Performance ◽  
Automata Network ◽  
Time Systems

In this paper we present a framework, an algorithm and a new tool for online testing of real-time systems based on symbolic techniques used in UPPAAL model checker. We extend UPPAAL timed automata network model to a test specification which is used to generate test primitives and to check the correctness of system responses including the timing aspects. We use timed trace inclusion as a conformance relation between system and specification to draw a test verdict. The test generation and execution algorithm is implemented as an extension to UPPAAL and experiments carried out to examine the correctness and performance of the tool. The experiment results are promising.

Technical and Engineering Decisions That Drive Choices for Predictive Analytics of Plant Data

2011 ◽  
Author(s):  
William Nieman
Keyword(s):  
Real Time ◽  
Predictive Analytics ◽  
Current Data ◽  
Operating Conditions ◽  
Maintenance Cost ◽  
Real Time Systems ◽  
Efficient Technology ◽  
Time Model ◽  
Trade Offs ◽  
Time Systems

Power generation has the goal of maximizing power output while minimizing operations and maintenance cost. The challenge for plant manager is to move closer to reliability limits while being confident the risks of any decision are understood. To attain their goals and meet this challenge they are coming to realize that they must have frequent, accurate assessment of equipment operating conditions, and a path to continued innovation-. At a typical plant, making this assessment involves the collection and effective analysis of reams of complex, interrelated production system data, including demand requirements, load, ambient temperature, as well as the dependent equipment data. Wind turbine health and performance data is available from periodic and real-time systems. To obtain the timeliest understanding of equipment health for all the key resources in a large plant or fleet, engineers increasingly turn to real-time, model-based solutions. Real-time systems are capable of creating actionable intelligence from large amounts and diverse sources of current data. They can automatically detect problems and provide the basis for diagnosis and prioritization effectively for many problems, and they can make periodic inspection methods much more efficient. Technology exists to facilitate prediction of when assets will fail, allowing engineers to target maintenance costs more effectively. But, it is critical to select the best predictive analytics for your plant. How do you make that choice correctly? Real-time condition monitoring and analysis tools need to be matched to engineering process capability. Tools are employed at the plant in lean, hectic environments; others are deployed from central monitoring centers charged with concentrating scarce resources to efficiently support plants. Applications must be flexible and simple to implement and use. Choices made in selection of new tools can be very important to future success of plant operations. So, these choices require solid understanding of the problems to be solved and the advantages and trade-offs of potential solutions. This choice of the best Predictive Analytic solution will be discussed in terms of key technology elements and key engineering elements.

scholarly journals Internet of Things (IoT) Platform for Multi-Topic Messaging

Energies ◽  
2020 ◽  
Vol 13 (13) ◽  
pp. 3346
Author(s):  
Mahmoud Hussein ◽  
Ahmed I. Galal ◽  
Emad Abd-Elrahman ◽  
Mohamed Zorkany
Keyword(s):  
Operating System ◽  
Internet Of Things ◽  
Real Time ◽  
Communication Protocol ◽  
Real Time Systems ◽  
Real Time System ◽  
Client Server ◽  
Iot Applications ◽  
Iot Platforms ◽  
Time Systems

IoT-based applications operate in a client–server architecture, which requires a specific communication protocol. This protocol is used to establish the client–server communication model, allowing all clients of the system to perform specific tasks through internet communications. Many data communication protocols for the Internet of Things are used by IoT platforms, including message queuing telemetry transport (MQTT), advanced message queuing protocol (AMQP), MQTT for sensor networks (MQTT-SN), data distribution service (DDS), constrained application protocol (CoAP), and simple object access protocol (SOAP). These protocols only support single-topic messaging. Thus, in this work, an IoT message protocol that supports multi-topic messaging is proposed. This protocol will add a simple “brain” for IoT platforms in order to realize an intelligent IoT architecture. Moreover, it will enhance the traffic throughput by reducing the overheads of messages and the delay of multi-topic messaging. Most current IoT applications depend on real-time systems. Therefore, an RTOS (real-time operating system) as a famous OS (operating system) is used for the embedded systems to provide the constraints of real-time features, as required by these real-time systems. Using RTOS for IoT applications adds important features to the system, including reliability. Many of the undertaken research works into IoT platforms have only focused on specific applications; they did not deal with the real-time constraints under a real-time system umbrella. In this work, the design of the multi-topic IoT protocol and platform is implemented for real-time systems and also for general-purpose applications; this platform depends on the proposed multi-topic communication protocol, which is implemented here to show its functionality and effectiveness over similar protocols.

scholarly journals Time Petri Nets with Action Duration

2013 ◽  
Vol 4 (2) ◽  
pp. 62-83 ◽  
Author(s):  
N. Belala ◽  
D.E. Saїdouni ◽  
R. Boukharrou ◽  
A.C. Chaouche ◽  
A. Seraoui ◽  
...  
Keyword(s):  
Petri Nets ◽  
Real Time ◽  
Timed Automata ◽  
Operational Semantics ◽  
Time Interval ◽  
Timing Constraints ◽  
Time Petri Nets ◽  
Real Time Systems ◽  
High Level ◽  
Time Systems

The design of real-time systems needs a high-level specification model supporting at the same time timing constraints and actions duration. The authors introduce in this paper an extension of Petri Nets called Time Petri Nets with Action Duration (DTPN) where time is associated with transitions. In DTPN, the firing of transitions is bound to a time interval and transitions represent actions which have explicit durations. The authors give an operational semantics for DTPN in terms of Durational Action Timed Automata (DATA). DTPN considers both timing constraints and durations under a true-concurrency semantics with an aim of better expressing concurrent and parallel behaviours of real-time systems.

Sign in / Sign up

Export Citation Format

Share Document