Skip to main content
Journal cover image

LCV: A verification tool for linear controller software

Publication ,  Conference
Park, J; Pajic, M; Sokolsky, O; Lee, I
Published in: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
January 1, 2019

In the model-based development of controller software, the use of an unverified code generator/transformer may result in introducing unintended bugs in the controller implementation. To assure the correctness of the controller software in the absence of verified code generator/transformer, we develop Linear Controller Verifier (LCV), a tool to verify a linear controller implementation against its original linear controller model. LCV takes as input a Simulink block diagram model and a C code implementation, represents them as linear time-invariant system models respectively, and verifies an input-output equivalence between them. We demonstrate that LCV successfully detects a known bug of a widely used code generator and an unknown bug of a code transformer. We also demonstrate the scalability of LCV and a real-world case study with the controller of a quadrotor system.

Duke Scholars

Published In

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

DOI

EISSN

1611-3349

ISSN

0302-9743

ISBN

9783030174613

Publication Date

January 1, 2019

Volume

11427 LNCS

Start / End Page

213 / 225

Related Subject Headings

  • Artificial Intelligence & Image Processing
  • 46 Information and computing sciences
 

Citation

APA
Chicago
ICMJE
MLA
NLM
Park, J., Pajic, M., Sokolsky, O., & Lee, I. (2019). LCV: A verification tool for linear controller software. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 11427 LNCS, pp. 213–225). https://doi.org/10.1007/978-3-030-17462-0_12
Park, J., M. Pajic, O. Sokolsky, and I. Lee. “LCV: A verification tool for linear controller software.” In Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 11427 LNCS:213–25, 2019. https://doi.org/10.1007/978-3-030-17462-0_12.
Park J, Pajic M, Sokolsky O, Lee I. LCV: A verification tool for linear controller software. In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 2019. p. 213–25.
Park, J., et al. “LCV: A verification tool for linear controller software.” Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 11427 LNCS, 2019, pp. 213–25. Scopus, doi:10.1007/978-3-030-17462-0_12.
Park J, Pajic M, Sokolsky O, Lee I. LCV: A verification tool for linear controller software. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 2019. p. 213–225.
Journal cover image

Published In

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

DOI

EISSN

1611-3349

ISSN

0302-9743

ISBN

9783030174613

Publication Date

January 1, 2019

Volume

11427 LNCS

Start / End Page

213 / 225

Related Subject Headings

  • Artificial Intelligence & Image Processing
  • 46 Information and computing sciences