RTCP-NET APPROACH TO VERIFICATION OF EMBEDDED SYSTEMS IMPLEMENTED IN ADA

The paper presents an RTCP-net approach to the verification of embedded systems implemented in Ada programming language. We focus on the verification of software implemented in accordance with Ada Ravenscar Profile. An RTCP-net model is constructed with the use of the Ada source code, and utilised for the formal verification of the software. An example of a driver for a home heating furnace is used to demonstrate the most important features of this approach.