NDLI: Formal verification of real-time systems with preemptive scheduling

Content Provider	Springer Nature Link
Author	Lime, Didier Roux, Olivier H.
Copyright Year	2008
Abstract	In this paper, we propose a method for the verification of timed properties for real-time systems featuring a preemptive scheduling policy: the system, modeled as a scheduling time Petri net, is first translated into a linear hybrid automaton to which it is time-bisimilar. Timed properties can then be verified using HyTech. The efficiency of this approach leans on two major points: first, the translation features a minimization of the number of variables (clocks) of the resulting automaton, which is a critical parameter for the efficiency of the ensuing verification. Second, the translation is performed by an over-approximating algorithm, which is based on Difference Bound Matrix and therefore efficient, that nonetheless produces a time-bisimilar automaton despite the over-approximation. The proposed modeling and verification method are generic enough to account for many scheduling policies. In this paper, we specifically show how to deal with Fixed Priority and Earliest Deadline First policies, with the possibility of using Round-Robin for tasks with the same priority. We have implemented the method and give some experimental results illustrating its efficiency.
Starting Page	118
Ending Page	151
Page Count	34
File Format	PDF
ISSN	09226443
Journal	Real-Time Systems
Volume Number	41
Issue Number	2
e-ISSN	15731383
Language	English
Publisher	Springer US
Publisher Date	2008-08-28
Publisher Place	Boston
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	Formal methods Petri nets Preemptive scheduling Verification Hybrid automata Control , Robotics, Mechatronics Communications Engineering, Networks Performance and Reliability Special Purpose and Application-Based Systems Computer Systems Organization and Communication Networks
Content Type	Text
Resource Type	Article
Subject	Control and Optimization Computer Networks and Communications Control and Systems Engineering Electrical and Electronic Engineering Computer Science Applications Modeling and Simulation

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Formal Verification of Real-time Systems with Preemptive Scheduling

Precautious-RM: a predictable non-preemptive scheduling algorithm for harmonic tasks

Schedulability analysis of non-preemptive strictly periodic tasks in multi-core real-time systems

The limited-preemptive feasibility of real-time tasks on uniprocessors

Verification and control of partially observable probabilistic systems

QoC elastic scheduling for real-time control systems

Compositional multiprocessor scheduling: the GMPR interface

Multiprocessor schedulability of arbitrary-deadline sporadic tasks: complexity and antichain algorithm

Efficient verification of distributed real-time systems with broadcasting behaviors

Formal verification of real-time systems with preemptive scheduling

Similar Documents

Formal Verification of Real-time Systems with Preemptive Scheduling

Precautious-RM: a predictable non-preemptive scheduling algorithm for harmonic tasks

Schedulability analysis of non-preemptive strictly periodic tasks in multi-core real-time systems

The limited-preemptive feasibility of real-time tasks on uniprocessors

Verification and control of partially observable probabilistic systems

QoC elastic scheduling for real-time control systems

Compositional multiprocessor scheduling: the GMPR interface

Multiprocessor schedulability of arbitrary-deadline sporadic tasks: complexity and antichain algorithm

Efficient verification of distributed real-time systems with broadcasting behaviors

Formal verification of real-time systems with preemptive scheduling