NDLI: Verifying distributed real-time properties of embedded systems via graph transformations and model checking

Content Provider	Springer Nature Link
Author	Madl, Gabor Abdelwahed, Sherif Schmidt, Douglas C.
Copyright Year	2006
Abstract	Component middleware provides dependable and efficient platforms that support key functional, and quality of service (QoS) needs of distributed real-time embedded (DRE) systems. Component middleware, however, also introduces challenges for DRE system developers, such as evaluating the predictability of DRE system behavior, and choosing the right design alternatives before committing to a specific platform or platform configuration. Model-based technologies help address these issues by enabling design-time analysis, and providing the means to automate the development, deployment, configuration, and integration of component-based DRE systems. To this end, this paper applies model checking techniques to DRE design models using model transformations to verify key QoS properties of component-based DRE systems developed using Real-time CORBA. We introduce a formal semantic domain for a general class of DRE systems that enables the verification of distributed non-preemptive real-time scheduling. Our results show that model-based techniques enable design-time analysis of timed properties and can be applied to effectively predict, simulate, and verify the event-driven behavior of component-based DRE systems.
Starting Page	77
Ending Page	100
Page Count	24
File Format	PDF
ISSN	09226443
Journal	Real-Time Systems
Volume Number	33
Issue Number	1-3
e-ISSN	15731383
Language	English
Publisher	Kluwer Academic Publishers
Publisher Date	2006-01-01
Publisher Place	Boston
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	Schedulability analysis Model checking Component middleware Distributed real-time Embedded systems Performance and Reliability Computer Systems Organization and Communication Networks Special Purpose and Application-Based Systems Communications Engineering, Networks Control Engineering
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

Efficient verification of distributed real-time systems with broadcasting behaviors

Schedulability analysis of a graph-based task model for mixed-criticality systems

Holistic schedulability analysis for multipacket messages in AFDX networks

Reduction-based schedulability analysis of distributed systems with cycles in the task graph

Hierarchical control of multiple resources in distributed real-time and embedded systems

A middleware model supporting time-triggered message-triggered objects for standard Linux systems

Service based meta-model for the development of distributed embedded real-time systems

Resource access control for dynamic priority distributed real-time systems

Schedulability analysis in hard real-time systems under thermal constraints

Verifying distributed real-time properties of embedded systems via graph transformations and model checking

Similar Documents

Efficient verification of distributed real-time systems with broadcasting behaviors

Schedulability analysis of a graph-based task model for mixed-criticality systems

Holistic schedulability analysis for multipacket messages in AFDX networks

Reduction-based schedulability analysis of distributed systems with cycles in the task graph

Hierarchical control of multiple resources in distributed real-time and embedded systems

A middleware model supporting time-triggered message-triggered objects for standard Linux systems

Service based meta-model for the development of distributed embedded real-time systems

Resource access control for dynamic priority distributed real-time systems

Schedulability analysis in hard real-time systems under thermal constraints

Verifying distributed real-time properties of embedded systems via graph transformations and model checking