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.

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.

Research on Security Level Assessment Technology in Embedded Real-Time System

2014 ◽  
Vol 696 ◽  
pp. 266-270
Author(s):  
Hong Li Chen
Keyword(s):  
Real Time ◽  
System Security ◽  
Assessment System ◽  
Security Level ◽  
Time System ◽  
Real Time System ◽  
Testing Environment ◽  
Simulation Testing ◽  
Time Systems ◽  
The Impact

This paper briefly describes the main ideas and implementation of technology strategy of Embedded real-time system security level assessment which is important part of mechanism to system flexibility based on embedded real-time system, designs the embedded real-time system security level assessment system based on pattern matching for the characteristics of embedded real-time systems. By building security level assessment system and simulation testing environment based on RT-Linux real-time operating system, the impact of Embedded real-time system security level assessment strategy on performance of RT-Linux was tested.

scholarly journals An Introduction to RTOS

2012 ◽  
pp. 285-289
Author(s):  
Sanjay Singh ◽  
Nishant Tripathi ◽  
Anil Kumar Chaudhary ◽  
Mahesh Kumar Singh
Keyword(s):  
Operating System ◽  
Real Time ◽  
Level Of Service ◽  
Real Time Systems ◽  
Time System ◽  
Real Time System ◽  
Real Time Operating System ◽  
System A ◽  
External Stimuli ◽  
Time Systems

RTOS (real time operating system) can be defined as “The ability of the operating system to provide a required level of service in bounded response time.” A real time system responds in a (timely) predictable way to unpredictable external stimuli arrivals. To build a predictable system, all its components (hardware & software) should enable this requirement to be fulfilled. Traffic on a bus for example should take place in a way allowing all events to be managed within the prescribe time limit. However it should not be forgotten that a good RTOS is only is building block. Using it in a wrongly designed system may lead to a malfunctioning of the RT system. A good RTOS can be defined as one that has a bounded (predictable) behavior under all system load scenarios (simultaneous interrupts and thread execution). In RT system, each individual deadline should be met. Real-time systems are designed to control and monitor their environment. Most of these systems are using sensors to collect environment state and use actuators to change something.

scholarly journals Real-Time System Modeling and Verification Through Labeled Transition System Analyzer

IEEE Access ◽  
2019 ◽  
Vol 7 ◽  
pp. 26314-26323
Author(s):  
Yilong Yang ◽  
Quan Zu ◽  
Wei Ke ◽  
Miaomiao Zhang ◽  
Xiaoshan Li
Keyword(s):  
Real Time ◽  
System Modeling ◽  
Transition System ◽  
Time System ◽  
Real Time System ◽  
Labeled Transition System

A Systematic Survey of Multiprocessor Real-Time Scheduling and Synchronization Protocol

2022 ◽  
Vol 12 ◽  
Author(s):  
Ajitesh Kumar
Keyword(s):  
Real Time ◽  
Rapid Development ◽  
Research Work ◽  
Resource Scheduling ◽  
Multiprocessor Scheduling ◽  
Shared Resources ◽  
Time System ◽  
Real Time System ◽  
Real Time Scheduling ◽  
Time Scheduling

Background: Nowadays, there is an immense increase in the demand for high power computation of real-time workloads and the trend towards multi-core and multiprocessor CPUs. The real-time system needs to be implemented upon multiprocessor platforms. Introduction: The nature of processors in an embedded real-time system is changing day by day. The two most significant challenges in a multiprocessor environment are scheduling and synchronization. The popularity of real-time multi-core systems has exploded in recent years, driving the rapid development of a variety of methods for multiprocessor scheduling of essential tasks, on the other hand, these systems have constraints when it comes to maintaining synchronization in order to access shared resources. Method: This research work presents a systematic review of different existing scheduling algorithms and synchronization protocols for shared resources in a real-time multiprocessor environment. The manuscript also presents a study based on various metrics of resource scheduling and comparison among different resource scheduling techniques. Result and Conclusion: The survey classifies open issues, key challenges, and likely useful research directions. Finally, we accept that there is still a lot of capacity in getting better resource management and further maintaining the overall quality. The paper considers such a future path of research in this field.

Sign in / Sign up

Export Citation Format

Share Document