Citation
Jyotirmoy Deshmukh. "Bridging the Gap between Research and Practice: Formal Methods in the Automotive Domain". Talk or presentation, 5, October, 2015.

Abstract
At the heart of an automobile are its engine and powertrain, and the operation of these components is controlled by embedded software on electronic control units (ECUs). The paradigm of model-based development (MBD) has become the de facto standard for designing such control software. MBD designs of control software range from feature-level models to application-level and even entire system-level models. On the other hand, models of the plant (e.g. the engine), can range from simple physics-based models to high-fidelity models incorporating test-data. The advantage of MBD is in its ability to design, validate, and analyze the closed-loop model of the plant and the controller, often well before the actual hardware components become available. Unfortunately, even the simplest closed-loop model of an automotive powertrain subsystem is a complex cyber-physical system with highly nonlinear and hybrid dynamics, and reasoning about the correctness of such closed-loop models is a formidable task. In this talk, we introduce two challenges in reasoning about industrial-scale closed-loop control models: (1) scaling verification or bug-finding techniques to engine control software, and (2) formalisms to express correctness and performance requirements for such models. We survey some of the existing work done to address such questions, and present some promising directions for future work.

Electronic downloads

• seminar.2015-10-05.Jyotirmoy_Deshmukh.pdf · application/pdf · 2467 kbytes

• HTML

  Jyotirmoy Deshmukh. <a
  href="http://chess.eecs.berkeley.edu/pubs/1121.html"
  ><i>Bridging the Gap between Research and Practice:
  Formal Methods in the Automotive Domain</i></a>,
  Talk or presentation,  5, October, 2015.

• Plain text

  Jyotirmoy Deshmukh. "Bridging the Gap between Research
  and Practice: Formal Methods in the Automotive Domain".
  Talk or presentation,  5, October, 2015.

• BibTeX

  @presentation{Deshmukh15_BridgingGapBetweenResearchPracticeFormalMethodsInAutomotive,
      author = {Jyotirmoy Deshmukh},
      title = {Bridging the Gap between Research and Practice:
                Formal Methods in the Automotive Domain},
      day = {5},
      month = {October},
      year = {2015},
      abstract = {At the heart of an automobile are its engine and
                powertrain, and the operation of these components
                is controlled by embedded software on electronic
                control units (ECUs). The paradigm of model-based
                development (MBD) has become the de facto standard
                for designing such control software. MBD designs
                of control software range from feature-level
                models to application-level and even entire
                system-level models. On the other hand, models of
                the plant (e.g. the engine), can range from simple
                physics-based models to high-fidelity models
                incorporating test-data. The advantage of MBD is
                in its ability to design, validate, and analyze
                the closed-loop model of the plant and the
                controller, often well before the actual hardware
                components become available. Unfortunately, even
                the simplest closed-loop model of an automotive
                powertrain subsystem is a complex cyber-physical
                system with highly nonlinear and hybrid dynamics,
                and reasoning about the correctness of such
                closed-loop models is a formidable task. In this
                talk, we introduce two challenges in reasoning
                about industrial-scale closed-loop control models:
                (1) scaling verification or bug-finding techniques
                to engine control software, and (2) formalisms to
                express correctness and performance requirements
                for such models. We survey some of the existing
                work done to address such questions, and present
                some promising directions for future work.},
      URL = {http://chess.eecs.berkeley.edu/pubs/1121.html}
  }
  

Posted by Sadigh Dorsa on 14 Oct 2015.
For additional information, see the Publications FAQ or contact webmaster at chess eecs berkeley edu.