Publication

From an Abstract Object-Oriented Model to a Ready-to-Use Embedded System Controller

Didier Buchs, Stanislav Chachkov
2001
Conference Papers

Abstract

We present an example of a construction of an embedded software system-a controller-from the formal specification to executable code. The CO-OPN (Concurrent Object Oriented Petri Net) formal specification language is used for modelling the controller and the associated hardware system with the inherent limitation of its physical components. CO-OPN formal language is based on coordinated algebraic Petri nets. The CO-OPN model can be used to verify some properties of the controller in the concrete physical environment. This is achieved by constrained animation of the valid prototype produced by automatic code generation. The possibility to incrementally refine the generated code can be used to obtain a more efficient implementation.

Official source

https://infoscience.epfl.ch/entities/publication/107f00e7-b232-4c8b-8495-bc89edc0a1ac

About this result

This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.

Graph Chat

Chat with Graph Search

Ask any question about EPFL courses, lectures, exercises, research, news, etc. or try the example questions below.

DISCLAIMER: The Graph Chatbot is not programmed to provide explicit or categorical answers to your questions. Rather, it transforms your questions into API requests that are distributed across the various IT services officially administered by EPFL. Its purpose is solely to collect and recommend relevant references to content that you can explore to help you answer your questions.

Didier Buchs, Stanislav Chachkov
2001
Conference Papers

Abstract

Official source

https://infoscience.epfl.ch/entities/publication/107f00e7-b232-4c8b-8495-bc89edc0a1ac

About this result

Related concepts (32)

Formal methods

In computer science, formal methods are mathematically rigorous techniques for the specification, development, analysis, and verification of software and hardware systems. The use of formal methods for software and hardware design is motivated by the expectation that, as in other engineering disciplines, performing appropriate mathematical analysis can contribute to the reliability and robustness of a design.

Specification language

A specification language is a formal language in computer science used during systems analysis, requirements analysis, and systems design to describe a system at a much higher level than a programming language, which is used to produce the executable code for a system. Specification languages are generally not directly executed. They are meant to describe the what, not the how. Indeed, it is considered as an error if a requirement specification is cluttered with unnecessary implementation detail.

Formal specification

In computer science, formal specifications are mathematically based techniques whose purpose are to help with the implementation of systems and software. They are used to describe a system, to analyze its behavior, and to aid in its design by verifying key properties of interest through rigorous and effective reasoning tools. These specifications are formal in the sense that they have a syntax, their semantics fall within one domain, and they are able to be used to infer useful information.

Related publications (7)

From an Abstract Object-Oriented Model to a Ready-to-Use Embedded System Controller

Chat with Graph Search

Practical Compositional Diagramming

Extending Safe C Support In Leon

From Formal Specifications to Ready-to-Use Software Components: The Concurrent Object-Oriented Petri Net Approach