*banner
 

Bridging the Gap between Research and Practice: Formal Methods in the Automotive Domain
Jyotirmoy Deshmukh

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

Citation formats  
  • 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.

Notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright.

©2002-2018 Chess