Citation
Christos Stergiou. "Schedulability and Verification of Real-Time Discrete-Event Systems". Talk or presentation, 16, September, 2013.

Abstract
Cyber-physical systems are systems where there is a tight interaction between the computing world and the physical world. In spite of the significance of time in the dynamics of the physical world, real-time embedded software today is commonly built using programming abstractions with little or no temporal semantics. PTIDES (Programming Temporally Integrated Distributed Embedded Systems) is a programming model whose goal is to address this problem. It proposes a model-based design approach for the programming of distributed real-time embedded systems, in which the timing of real-time operations is specified as part of the model. This is accomplished by using as an underlying formalism a discrete-event (DE) model of computation, which is extended with real-time semantics. We address the schedulability question for PTIDES programs and uniprocessor platforms. A PTIDES program is schedulable if for all legal sensor inputs, there exists a scheduling of the PTIDES components that meets all the specified deadlines. The timing specifications allowed in the discrete-event formalism can be seen as a generalization of end-to-end latencies which are usually studied in the hard real-time computing literature. This results in a rather idiosyncratic schedulability problem. We first show that for a large subset of discrete-event models, the earliest-deadline-first scheduling policy is optimal. Second, we show that all but a finite part of the infinite state space of a PTIDES execution results in demonstrably unschedulable behaviors. As a result the schedulability problem can be reduced to a finite-state reachability problem. We describe this reduction using timed automata. We next turn to the verification problem for DE systems themselves. We study a basic deterministic DE model, where actors are simple constant-delay components, and two extensions of it: first, one where actors are not constant but introduce non-deterministic delays, and second, one where actors are either deterministic delays or are specified using timed automata. We investigate verification questions on DE models and examine expressiveness relationships between the DE models and timed automata. Finally, we discuss extensions of this work to cover a wider range of discrete-event actors, and propose an approach to design more efficient and practical analyses for schedulability testing.

Electronic downloads

• christos-stergiou-schedulbility_and_verification_of_rt_de_sys-talk_sep_16.pdf · application/pdf · 1332 kbytes

• HTML

  Christos Stergiou. <a
  href="http://chess.eecs.berkeley.edu/pubs/1017.html"
  ><i>Schedulability and Verification of Real-Time
  Discrete-Event Systems</i></a>, Talk or
  presentation,  16, September, 2013.

• Plain text

  Christos Stergiou. "Schedulability and Verification of
  Real-Time Discrete-Event Systems". Talk or
  presentation,  16, September, 2013.

• BibTeX

  @presentation{Stergiou13_SchedulabilityVerificationOfRealTimeDiscreteEventSystems,
      author = {Christos Stergiou},
      title = {Schedulability and Verification of Real-Time
                Discrete-Event Systems},
      day = {16},
      month = {September},
      year = {2013},
      abstract = {Cyber-physical systems are systems where there is
                a tight interaction between the computing world
                and the physical world. In spite of the
                significance of time in the dynamics of the
                physical world, real-time embedded software today
                is commonly built using programming abstractions
                with little or no temporal semantics. PTIDES
                (Programming Temporally Integrated Distributed
                Embedded Systems) is a programming model whose
                goal is to address this problem. It proposes a
                model-based design approach for the programming of
                distributed real-time embedded systems, in which
                the timing of real-time operations is specified as
                part of the model. This is accomplished by using
                as an underlying formalism a discrete-event (DE)
                model of computation, which is extended with
                real-time semantics. We address the schedulability
                question for PTIDES programs and uniprocessor
                platforms. A PTIDES program is schedulable if for
                all legal sensor inputs, there exists a scheduling
                of the PTIDES components that meets all the
                specified deadlines. The timing specifications
                allowed in the discrete-event formalism can be
                seen as a generalization of end-to-end latencies
                which are usually studied in the hard real-time
                computing literature. This results in a rather
                idiosyncratic schedulability problem. We first
                show that for a large subset of discrete-event
                models, the earliest-deadline-first scheduling
                policy is optimal. Second, we show that all but a
                finite part of the infinite state space of a
                PTIDES execution results in demonstrably
                unschedulable behaviors. As a result the
                schedulability problem can be reduced to a
                finite-state reachability problem. We describe
                this reduction using timed automata. We next turn
                to the verification problem for DE systems
                themselves. We study a basic deterministic DE
                model, where actors are simple constant-delay
                components, and two extensions of it: first, one
                where actors are not constant but introduce
                non-deterministic delays, and second, one where
                actors are either deterministic delays or are
                specified using timed automata. We investigate
                verification questions on DE models and examine
                expressiveness relationships between the DE models
                and timed automata. Finally, we discuss extensions
                of this work to cover a wider range of
                discrete-event actors, and propose an approach to
                design more efficient and practical analyses for
                schedulability testing. },
      URL = {http://chess.eecs.berkeley.edu/pubs/1017.html}
  }
  

Posted by Armin Wasicek on 16 Sep 2013.
Groups: chessworkshop
For additional information, see the Publications FAQ or contact webmaster at chess eecs berkeley edu.