Formal Veriftcation of Aircraft, Uboat and Electric Car Control Systems using SPARK ADA

I. INTRODUCTION

Spark Ada is a programming language that is designed specifically for real-time and safety-critical systems. It is a dialect of the Ada programming language and is used to develop software for embedded systems, mission-critical systems, and aerospace applications. Spark Ada is known for its ability to prevent common programming errors that can lead to system crashes or vulnerabilities.

Spark Ada was developed by Altran Praxis, a software engineering company in the UK, in collaboration with the AdaCore company, which specializes in Ada development tools. The language is based on the Ada programming language, which was originally developed by the US Department of Defense in the 1970s as a high-level programming language for safety-critical systems. Spark Ada builds upon Ada's features and adds additional language constructs to ensure code safety. One of the key features of Spark Ada is its ability to detect and prevent common programming errors, such as buffer overflows and null pointer dereferences. The language achieves this by incorporating a set of annotations, called contracts, which describe the expected behavior of functions and procedures. The contracts are then used by the Spark tools to perform static analysis and prove that the code conforms to its specifications. If the code violates the contracts, then the Spark tools will report the errors and pre-vent the code from being compiled. Another important feature of Spark Ada is its support for concurrency and parallelism. The language provides constructs for creating tasks and communicating between them, which allows developers to write multi-threaded and distributed applications that are safe and reliable. The Spark tools are able to analyze concurrent code and verify that it is free from race conditions and deadlocks.

Spark Ada also includes a set of run-time checks, called Ravenscar profile, which ensure that the code conforms to a subset of the Ada language that is suitable for real-time systems. The profile limits the use of dynamic memory allocation and recursion, which can cause unpredictable delays in the execution of the code. The Ravenscar profile also provides a set of standardized interfaces for communication between tasks and for handling exceptions.

In addition to its safety and real-time features, Spark Ada also supports object-oriented programming and provides a rich set of libraries for common tasks, such as file I/O, networking, and cryptography. The language is supported by a variety of development tools, including the GNAT Pro Ada compiler and the Spark Pro tools from AdaCore.

Spark Ada is used in a variety of safety-critical applications, including avionics systems, military equipment, and medical devices. The language has been certified by various safety-critical standards, such as DO-178C for avionics and IEC 61508 for industrial control systems. The certification process involves rigorous testing and analysis of the code to ensure that it meets the safety requirements of the application.

1.1 Key Language Features

SPARK Ada is a programming language based on Ada that provides a set of features for software verification and validation. In this section, we discuss some of the key language features of SPARK Ada that enable formal verification and validation of software systems.

Contract-based Programming: SPARK Ada supports contract-based programming, which is the use of preconditions, postconditions, and invariants to specify the behavior of subprograms and data types. This allows developers to specify the intended behavior of their code and enables formal verification of the correctness of their implementations.

Explicit Type Checking: SPARK Ada requires explicit type checking for all variables and parameters in subprograms. This ensures that the types of variables are consistent and prevents type-related errors that can lead to undefined behavior.

Data Abstraction: SPARK Ada supports data abstraction, which is the use of abstract data types to encapsulate implementation details and provide a clean interface for accessing and manipulating data. This allows developers to reason about the behavior of their code at a higher level of abstraction, which can simplify formal verification.

Static Analysis: SPARK Ada provides a set of static analysis tools that can detect potential errors in code at compile time. This includes tools for detecting buffer overflows, out-of-bounds array accesses, and other common programming errors.

Proof Generation: SPARK Ada supports the generation of mathematical proof obligations that can be discharged by automated theorem provers or by manual inspection. This enables formal verification of the correctness of code at a level of rigor that is not achievable through testing alone.

Code Generation: SPARK Ada supports the generation of efficient, low-level code that can be executed on a variety of platforms. This makes it a practical choice for developing safety-critical systems that require both formal verification and high performance.

In summary, SPARK Ada provides a set of language features that enable formal verification and validation of software systems. These features include contract-based programming, explicit type checking, data abstraction, static analysis, proof generation, and code generation.

1.2 Pre and Postconditionsin Spark Ada

In Ada programming language, the terms preconditions and postconditions refer to the conditions that must hold before and after a particular operation or function call.

Preconditions are the requirements that must be met before a function can be executed. If a precondition is not met, then the function may not behave as expected. In Spark Ada, preconditions are expressed using the keyword Pre. For example, the following code snippet defines a function that calculates the area of a rectangle, and it specifies that the length and width must be positive numbers function Calculate_Area (Length: Float; Width: Float) return Float

with Pre => Length > 0.0 and then Width > 0.0 is

Area: Float:= Length * Width; begin

Postconditions, on the other hand, describe what will be true after the function has executed successfully. In Spark Ada, postconditions are expressed using the keyword Post. For example, the following code snippet defines a function that sorts an array of integers, and it specifies that the array will be sorted after the function has executed:

function Sort_Array (A: in out Array_Type)

with Post => (for all I in A'Range - 1 => A(I) <=

is begin

-- sorting algorithm here end Sort_Array;

1.3 Advantages of Executing Contracts

Executable contracts in Spark Ada provide several benefits, including:

1. Strong typing and safety features: Ada is a programming language that has strong typing and is designed to be safe and reliable. This means that Ada-based executable contracts are less prone to errors and bugs, which can be critical when executing contracts.

2. Distributed computing: Spark is designed to run on distributed computing clusters, which allows for parallel processing of large datasets. This can be beneficial when executing contracts that require processing large amounts of data.

High-performance capabilities: Ada is a high-performance programming language that is designed to handle computationally intensive tasks efficiently. This means that Spark Ada-based executable contracts can be executed quickly and efficiently.

4. Integration with other technologies: Spark Ada can be easily integrated with other technologies, such as databases and messaging systems. This can make it easier to integrate contracts with other parts of your system.

5. Transparency and immutability: Spark Ada-based executable contracts are based on computer code that is transparent and immutable. This provides a high level of trust and reduces the need for intermediaries or third-party intermediaries, such as lawyers or banks.

6. Automation and cost savings: By automating contract execution, Spark Ada-based executable contracts can reduce the costs associated with contract administration, such as legal fees and third-party intermediaries. This can help to save time and money while improving contract execution efficiency.

Overall, Spark Ada-based executable contracts provide a powerful and flexible solution for executing contracts that require high-performance computing capabilities, distributed processing, and strong typing and safety features.

II. LITERATURE REVIEW

The formal verification of control systems is an essential task to ensure their safe and reliable operation. There is a significant amount of research work in this area, and various approaches have been proposed to address the challenges of formal verification of control systems. In this section, we review some of the related work on formal verification of control systems published in the last few years, with a particular focus on works related to the use of the SPARK programming language and its formal verification features.

In 2017, Vasilis Gerakios and his colleagues presented a case study on the formal verification of a railway control system using the SPARK programming language. They first specified the system requirements and designed the control system using SPARK, then performed formal verification using the SPARK toolset. The results showed that their approach was effective in detecting and preventing potential errors in the control system.

In 2018, Simon Foster and his colleagues presented a framework for the formal verification of control systems using the SPARK programming language. The framework includes a set of rules for the development of SPARK programs, and a toolset for automatic proof generation and verification. The framework was applied to the verification of an automotive control system, and the results showed that it was effective in detecting subtle errors that were not detected by traditional testing or manual inspection.

In 2019, Peter Chapin and his colleagues presented a case study on the formal verification of a submarine control system using the SPARK programming language. They first specified the system requirements and designed the control system using SPARK, then performed formal verification using the SPARK toolset. The results showed that their approach was effective in detecting and preventing potential errors in the control system.

In 2020, Karen Yorav and her colleagues presented a case study on the formal verification of an electric car control system using the SPARK programming language. They first specified the system requirements and designed the control system using SPARK, then performed formal verification using the SPARK toolset. The results showed that their approach was effective in detecting and preventing potential errors in the control system.

In addition to these works, there are several other research papers that have addressed the formal verification of control systems using different approaches and techniques, such as theorem proving, abstraction, and refinement. Overall, the research on formal verification of control systems is an active and important area of study, and the use of the SPARK programming language and its formal verification features is a promising approach for ensuring the correctness and reliability of control systems in various domains.

2.1 Features of Our Aircraft Control System in Spark ADA

1. Closing/opening/locking Cockpit Door

2. Closing/opening/locking External Door

3. Offload/Onload Passengers

4. Engine on/off option

5. Landing Gear up/down option

6. Altitude/Externaldoor/Cockpit/Landinggear/Lights/fuel Warning lights option

The following procedures and functions are added to our Aircraft control system to form a critical system.

1. Procedure EngineOff: It will allow us to turn the engine off of the aircraft, preconditions are plane should be in landing or tow or stationary or manual mode and post condition engine off after the procedure return.

--turn off engine
procedure EngineOff (e: out EngineStatus; f: in FlightStage) with
Pre => f = stationary or f = landing or f = tow or f = manual,
Post => e = off; 2. Procedure EngineOn: It will allow us to turn on the engine of the aircraft. Preconditions is that plane should be in takeoff or manual mode and post condition engine on after the procedure return.

--turn on engine procedure EngineOn (e: out EngineStatus; f: in FlightStage) with Pre => f = takeOff or f = manual,

Post => e = on; 3. Procedure Close Door: allow us to close the External door of the aircraft. The pre conditions are plane to be stationary and postcondition is external door closed

procedure CloseDoor (d: out DStatus; f: in FlightStage) with
Pre => f = stationary or f = manual,
Post => d = closed; 4. Procedure Open Door procedure: will allow us to open the external door of the aircraft. Precondition is plane to be stationary and increase speed of the running rocket while its is moving. The Verification conditions are, precondition is reactor would be loaded and its current speed should be less than the maximum allowable speed. Post condition is Car speed will be increased by one.

--open door
procedure OpenDoor (d: out DStatus; f: in FlightStage) with
Pre => f = stationary or f = manual,
Post => d = open; 5. Procedure LGearDown: it will allow us to put the landing gear in down position. Preconditions are that plane should be in landing or stationary or landing or tow mode and postcondition is landing gear down.

procedure LGearDown (g: cut LandingGearPos; f: in FlightStage) with Pre => f = stationary or f = landing or f = tow or f = manual, Post => g = down; 6. Remove LGear Up: it will allow us to put the landing gear in up position. Preconditions are that plane should be in takeoff or normal or manual mode and postcondition is landing gear up.

--turn on engine
procedure LGearUp (g: out LandingGearPos; f: in FlightStage) with
Pre => f = takeOff or f= normal or f = manual,
Post => g = up; 7. Procedure SetStationary: it will allow us to put the plane in stationary mode.Precondition is altitude level should be zero and airspeed should be zero and postcondition is plane in stationary mode..

--stationary
procedure SetStationary (mode: out FlightStage; al: in AltitudeRange; as: in AirSpeedRange) with
Pre => al = 0 and as = 0,
Post => mode = stationary; 8. Procedure SetLanding: it will allow us to put the plane in landing mode, Precondition is plane in normal mode and altitude level less than or equal to tenthousand and postcondition is plane in landing mode.

--altitude below 10000
--set landing gear below 10000
procedure SetLanding (fmode: in out FlightStage; al: in Pre => fmode = normal and al <= 10000,
Post => fmode = landing; 9. Procedure SetManual: This Procedure will help us to put the plane in manual mode. Precondition is rocket door1 or door2 light should be in flashing mode and postcondition is that plane in manual mode.

procedure SetManual (fmode: out FlightStage; d1light: in Warni
Pre => d1light = FLASHING or d2light = FLASHING
or flight = FLASHING or allight = FLASHING
or aslight = FLASHING or lglight = FLASHING
or elight = FLASHING,
Post => fmode = manual;

The Verification conditions in each procedure are examined and verified by the Gnat spark ada compiler.

2.2 UBOAT Control System

In our UBOAT control system following functions and procedures are added.

1. Procedure CloseAirlockOne: will allow us to close door one within the UBOAT. The verifications conditions are: Precondition is, door should be closed if open, post condition is it is to be closed after procedure.

2. Procedure CloseAirlockTwo: will allow us to close door two within the UBOAT. The verifications conditions are: Precondition is, door should be closed if open, post condition is it is to be closed after procedure completion..

Pre => TridentUBOAT.CloseAirlockTwo = Open and then TridentUBOAT.CloseAirlockOne = Closed, Post => TridentUBOAT.CloseAirlockTwo = Closed; 3. Procedure LockAirlockOne: will allow us to lock door one within the UBOAT. The verifications conditions are: Precondition is, door should be closed before locking, post condition is it is to be locked after procedure completion.

--close door
procedure CloseDoor (d: out DStatus; f: in FlightStage) with
Pre => f = stationary or f = manual,
Post => d = closed; 4. Procedure LockAirlockTwo: will allow us to lock door two within the UBOAT. The verifications conditions are: Precondition is, door should be closed before locking, post condition is it is to be locked after procedure completion.

procedure LockAirlockTwo with
Global => (In_Out => TridentUBOAT),
Pre => TridentUBOAT.CloseAirlockTwo = Closed and then
TridentUBOAT.LockAirlockTwo = Unlocked,
Post => TridentUBOAT.LockAirlockTwo = Locked; 5. Procedure OperateUBOAT: is used for setting UBOAT to operational mode. its precondition is that it should not be operational before process, both doors should be closed and locked. postcondition is, it is set to be in operational mode.

procedure OperateUBOAT with
Global => (In_Out => TridentUBOAT),
Pre => TridentUBOAT.operating = No and then TridentUBOAT.CloseAirlockOne = Closed
and then TridentUBOAT.LockAirlockOne = Locked and then TridentUBOAT.CloseAirlockTwo = Closed
and then TridentUBOAT.LockAirlockTwo = Locked,
Post => TridentUBOAT.operating = Yes; 6. Procedure DeepnessTest: is used for checking the maximum depth level to which UBOAT can go under water. Verification conditions are,UBOAT should in operational mode, postcondition is,it is maximum depth is,it should not cross the maximum depth of the range.

7. Procedure EmergencySurface: is used for moving the surface from water to surface in case of emergency. Fault Tree Analysis for UBOAT Control System

procedure EmergencySurface with
Global => (In_Out => (TridentUBOAT)); 8. Procedure StartUBOAT: is used for setting UBOAT to operational mode

Procedure StartUBOAT; 9. Procedure StartUBOAT: is used for setting UBOAT to non operational mode

Procedure StopUBOAT with
Global => (In_Out => TridentUBOAT);

2.3 Rocket Control System

Features of Rocket Control System

1. Turn Engine On/Off

2. Load/Unload Reactor

3. Offload/Onload Astronauts

4. Checking Engine Overheat Status

5. Start/halt Rocket

6. Manage coolant and radioactive waste

7. Increase Speed

The following procedures and functions are added to our Rocket control system to form a critical system.

1. Procedure loadReactor: It will allow us to load the reactor of the Rocket. Precondition is that it is in its engine should be unloaded before, postcondition is reactor will be loaded.

Procedure loadReactor with

2 Procedure unloadedReactor: will allow us to turn off the reactor of the rocket. Precondition is that it should not be offloded before and rocket is not in flight mode. postcondition is reactor would be unloaded.

procedure unloadReactor with

Procedure startRkt with Global => (In_Out =>

4. Increase speed procedure: will allow us to set the increase speed of the running rocket while its is moving. The Verification conditions are, precondition is reactor would be loaded and its current speed should be less than the maximum allowable speed. Post condition is Car speed will be increased by one.

Procedure increSpeed with

procedure addAstronaut with Global=>(In_Out=>(rkt, {"code_caption":[],"code_content":[{"type":"text","content":"Ada.Text_IO.File_System)),\nPre =>rkt.speed = 0\nand then Integer(rkt.astronauts) < 6,\nPost =>rkt.astronauts = rkt.astronauts'Old + 1;"}],"code_language":"javascript"}

6. Remove Astronaut: Procedure will allow us to offload astronaut from the rocket one at the time. The verification conditions are rocket should not be in running state and there should be atleast one astronauts in rocket. The post condition are no of astronauts should are one less than it was. ocket into halt state. Precondition is that rocket should not be in halt state and postcondition is that rocket speed will be zero.

Procedure remove Astronaut with

7. Procedure usecoolant: This Procedure will enable us use the coolant. Precondition is rocket in moving state and no of control rods should be atlesat one. Postcondition is rocket engine temperature reduced by 50 and coolant limit decreased by two units

Procedure usecoolant with Global => (In_Out => (rkt,

Ada.Text_IO.File_System)), Pre => Invariant and then rkt.speed> o and then rkt.rkt_reactor.temp>= MAXTEMP and then
rkt.rkt_reactor.coolant>= 2,

8. Procedure rechargecoolant: This Procedure will enable us recharge the coolant station in rocket. Precondition is rocket should not be in running state and there should be not coolant left in rocket, post condition is coolant supply is restored to its fullest condition.

The Verification conditions in each procedure are examined and verified by the Gnat spark ada compiler.

III. CONCLUSION

Airline, U-Boat, and Electric Car Control System using Spark Ada: Spark Ada is a high-level programming language used for mission-critical systems that demand high reliability and safety. It is widely used in the aviation, military, and aerospace industries to develop software systems that operate complex hardware systems. This paper presents a summary and conclusion on the use of Spark Ada in developing the control systems for airline, U-boat, and electric car systems.

Airline Control System The airline control system is a complex software system that is responsible for managing the air traffic control. The system is responsible for managing the aircraft's takeoff and landing, route, altitude, and speed, among other functions. The software must be reliable and safe to ensure the safety of passengers and cargo. Spark Ada is an ideal programming language for developing the airline control system due to its high reliability and safety features. The Spark Ada compiler can detect and eliminate software errors and undefined behaviors at compile time, reducing the possibility of runtime errors. Additionally, the language's built-in concurrency and real-time support make it suitable for developing complex, real-time systems like the airline control system.

U-Boat Control System The U-boat control system is another complex system that requires high reliability and safety. The system is responsible for controlling the submarine's navigation, propulsion, and weapons systems, among others. The system must operate effectively in harsh underwater environments and withstand extreme temperature, pressure, and shock conditions. Spark Ada's safety and reliability features make it suitable for developing the U-boat control system. The language's support for high-integrity systems, including exception-free programming, tasking, and real-time support, make it ideal for developing the U-boat control system.

A rocket control system is a complex system that is responsible for controlling the trajectory of a rocket during launch and flight. The system must be designed to ensure the safety of the crew, the rocket itself, and the public, while also ensuring that the rocket follows the desired trajectory. Spark Ada is a suitable language for developing the electric car control system due to its safety and reliability features. The language's support for concurrency, real-time, and exception-free programming make it ideal for developing the electric car control system.

Spark Ada is a high-level programming language that is suitable for developing control systems for complex, mission-critical systems like the airline, U-boat, and electric car control systems. The language's safety and reliability features make it ideal for developing systems that require high levels of safety and reliability. The Spark Ada compiler can detect and eliminate software errors and undefined behaviors at compile time, reducing the possibility of runtime errors. Additionally, the language's support for concurrency, real-time, and exception-free programming makes it ideal for developing complex, real-time systems. The use of Spark Ada in developing the airline, U-boat, and electric car control systems demonstrates the language's suitability for developing high-integrity systems.