Sound code generation from communicating hybrid models

Yerang Hur, Jesung Kim, Insup Lee, Jin Young Choi

Research output: Chapter in Book/Report/Conference proceedingChapter

11 Citations (Scopus)

Abstract

Precise translation from hybrid models to code is difficult because models are defined in the continuous-time domain whereas code executes on digital computers in a discrete fashion. Traditional approach is to associate the model with a sampling rate before code generation, and rely on an approximate algorithm that computes the next state numerically. Depending on the choice of the sampling rate and the algorithm, the behavior of the code may vary significantly due to numerical errors, but the discrepancy has been addressed informally, making the analysis results at the model level less meaningful for implementation. Formal relationship between the model and the code becomes even more unclear when components of the code execute concurrently. In this paper, we propose a formal framework that addresses the issue of soundness of concurrent programs generated from communicating hybrid models. The motivation is that concurrent programs executing in different rates may cause an erroneous transition when transition conditions are evaluated using values from different time instances. The essence of our technique is to refine the model by tightening transition conditions according to the maximum errors due to different sampling rates. We claim that the generated code has a trace of discrete transitions that is equivalent to one of the traces observable from the model, and that the values of variables are bounded. Our framework demonstrates how hybrid models defined in the continuous time domain are translated into discretized models with or without consideration of errors due to asynchronous sampling, and finally into executable code with real-time scheduling.

Original languageEnglish
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
EditorsRajeev Alur, George J. Pappas
PublisherSpringer Verlag
Pages432-447
Number of pages16
ISBN (Print)3540212590, 9783540212591
DOIs
Publication statusPublished - 2004

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume2993
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Sound code generation from communicating hybrid models'. Together they form a unique fingerprint.

  • Cite this

    Hur, Y., Kim, J., Lee, I., & Choi, J. Y. (2004). Sound code generation from communicating hybrid models. In R. Alur, & G. J. Pappas (Eds.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (pp. 432-447). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2993). Springer Verlag. https://doi.org/10.1007/978-3-540-24743-2_29