Towards safe embedded systems: Industrialc translational semantics for avr microcontrollers

Research output: Chapter in Book/Report/Conference proceedingConference contributionResearchpeer-review

Abstract

Embedded systems based on small cheap microcontrollers surround all aspects of our lives. Due to inherent concurrency microcontroller software can exhibit complex behavior that is best specified using specialized programming langauges. The IndustrialC language has been successfully used in a number of embedded appications and has proven useful for specification of complex reactive systems within the constrained computational capabilities of 8-bit microcontrollers. Many microcontroller-based systems are considered safety-critical and the safety of microcontroller software can only be assured using formal verification methods such as deductive verification and model checking. These methods require programming language semantics to be specified formally and unambiguously, yet the nature of microcontroller programming is such that program semantics differs even between CPU architectures and chip models. We present a translational semantics for IndustrialC in application to AVR-family microcontrollers that uses AVR Libc as a denotational metalanguage along with plain C constructs and discuss the benefits and pitfalls of the approach.

Original languageEnglish
Title of host publicationSIBIRCON 2019 - International Multi-Conference on Engineering, Computer and Information Sciences, Proceedings
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages857-861
Number of pages5
ISBN (Electronic)9781728144016
DOIs
Publication statusPublished - Oct 2019
Event2019 International Multi-Conference on Engineering, Computer and Information Sciences, SIBIRCON 2019 - Novosibirsk, Russian Federation
Duration: 21 Oct 201927 Oct 2019

Publication series

NameSIBIRCON 2019 - International Multi-Conference on Engineering, Computer and Information Sciences, Proceedings

Conference

Conference2019 International Multi-Conference on Engineering, Computer and Information Sciences, SIBIRCON 2019
CountryRussian Federation
CityNovosibirsk
Period21.10.201927.10.2019

Keywords

  • embedded systems
  • IndustrialC
  • safety-critical software
  • translational semantics

OECD FOS+WOS

  • 1.02 COMPUTER AND INFORMATION SCIENCES
  • 1.01 MATHEMATICS

Fingerprint

Dive into the research topics of 'Towards safe embedded systems: Industrialc translational semantics for avr microcontrollers<sup>∗</sup>'. Together they form a unique fingerprint.

Cite this