Title :
An approach to generating C code with proven LTL-based properties
Author_Institution :
University of West Bohemia, Department of Computer Science and Engineering, Pilsen, Czech Republic
fDate :
4/1/2011 12:00:00 AM
Abstract :
This paper presents a novel approach to software development, mainly useful for embedded devices. Embedded software is described in a programming language with very high level of abstraction. We first generate a special verifiable code from the description and prove that it has certain properties defined by LTL formulae. Then we generate the final C code with the same properties.
Keywords :
"Java","Programming","Embedded software","Cameras","Instruction sets","Embedded systems"
Conference_Titel :
EUROCON - International Conference on Computer as a Tool (EUROCON), 2011 IEEE
Print_ISBN :
978-1-4244-7486-8
DOI :
10.1109/EUROCON.2011.5929273
