NDLI: Schedulability and end-to-end latency in distributed ECU networks: formal modeling and precise estimation

Please wait, while we are loading the content...

Automatic verification of control system implementations

Parallelizing the H.264 decoder on the cell BE architecture

Online robust optimization framework for QoS guarantees in distributed soft real-time systems

Modeling buffers with data refresh semantics in automotive architectures

Using NAND flash memory for executing large volume real-time programs in automotive embedded systems

A unifying view of loosely time-triggered architectures

Model-based implementation of real-time applications

Power-aware temporal isolation with variable-bandwidth servers

Model-based analysis, synthesis and testing of automotive hardware/software architectures

A marketplace for cloud resources

Switching logic synthesis for reachability

Optimal WCET-aware code selection for scratchpad memory

Load-based schedulability analysis of certifiable mixed-criticality systems

Schedulability and end-to-end latency in distributed ECU networks: formal modeling and precise estimation

Janus-FTL: finding the optimal point on the spectrum between page and block mapping schemes

Semantics-preserving implementation of synchronous specifications over dynamic TDMA distributed architectures

Model-based specification of timing requirements

Resource adaptations with servers for hard real-time systems

Quantitative system validation in model driven design

Online stability validation using sector analysis

A model based approach for debugging embedded systems in real-time

Reducing stack with intra-task threshold priorities in real-time systems

TeleScribe: a scalable, resumable wireless reprogramming approach

A reliable MTD design for MLC flash-memory storage systems

From high-level component-based models to distributed implementations

Initiating a design pattern catalog for embedded network systems

Energy-aware packet and task co-scheduling for embedded systems

Components, platforms and possibilities: towards generic automation for MDA

PinaVM: a systemC front-end based on an executable intermediate representation

Nucleos: a runtime system for ultra-compact wireless sensor nodes

Ptera: an event-oriented model of computation for heterogeneous systems

Dynamic tuning of feature set in highly variant interactive applications

Schedulability and end-to-end latency in distributed ECU networks: formal modeling and precise estimation

Content Provider	ACM Digital Library
Author	Rajeev, A. C. Chokshi, Devesh B. Mohalik, Swarup Ramesh, S. Dixit, Manoj G.
Abstract	Embedded control systems in automobiles are typically implemented by a set of tasks deployed on multiple Electronic Control Units (ECUs) communicating via one or more buses like CAN or FlexRay. In the case of safety-critical systems, there are hard real-time bounds on the (i) response times of tasks/messages, and (ii) end-to-end latencies of certain task/message chains. These depend on various factors like the number of tasks (and messages) involved in the processing (and communication) sequence, parameters of these tasks/messages, scheduling policies, communication protocols, clock drifts, etc. Moreover, since the data transfer among tasks/messages is typically via asynchronous buffers that are overwritable and sticky, multiple semantics are possible for end-to-end latency. Hence, precise estimation of response times and end-to-end latencies in embedded systems is a non-trivial problem. In this paper, we propose a model-checking based technique to compute worst-case response times and end-to-end latencies. We consider a distributed system made of preemptively scheduled tasks and non-preemptively scheduled messages. Given a chain in the system, we estimate two different end-to-end latencies --LIFO and LILO-- which are important in automotive domain. From a system description, we automatically synthesize a formal model based on a discrete event simulation formalism called Calendar Automata. It is then model-checked to compute response times and end-to-end latencies. Our technique is more scalable than the existing formal methods based techniques. We have illustrated this technique on reasonably large case-studies from the automotive domain.
Starting Page	129
Ending Page	138
Page Count	10
File Format	PDF
ISBN	9781605589046
DOI	10.1145/1879021.1879039
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2010-10-24
Publisher Place	New York
Access Restriction	Subscribed
Subject Keyword	Calendar automata End-to-end latency Model-checking Schedulability
Content Type	Text
Resource Type	Article

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

Model checking based analysis of end-to-end latency in embedded, real-time systems with clock drifts

Model checking based analysis of end-to-end latency in embedded, real-time systems with clock drifts

Scalable model-checking for precise end-to-end latency computation

Model checking UML statecharts

Schedulability Analysis for Distributed Systems Using Network of Action Automata and Environment Automata

Timing Analysis of Distributed End-to-End Task Graphs with Model-Checking

Toward Formal Verification of ECU for Gasoline Direct Injection Engines

Formal Estimation of Worst-Case Communication Latency in a Network-on-Chip

Factored Planning: From Automata to Petri Nets

Schedulability and end-to-end latency in distributed ECU networks: formal modeling and precise estimation

Similar Documents

Model checking based analysis of end-to-end latency in embedded, real-time systems with clock drifts

Model checking based analysis of end-to-end latency in embedded, real-time systems with clock drifts

Scalable model-checking for precise end-to-end latency computation

Model checking UML statecharts

Schedulability Analysis for Distributed Systems Using Network of Action Automata and Environment Automata

Timing Analysis of Distributed End-to-End Task Graphs with Model-Checking

Toward Formal Verification of ECU for Gasoline Direct Injection Engines

Formal Estimation of Worst-Case Communication Latency in a Network-on-Chip

Factored Planning: From Automata to Petri Nets

Schedulability and end-to-end latency in distributed ECU networks: formal modeling and precise estimation