Software specification made funny with functional programming: Haskell as a kind of formal method! Some concrete examples.
Software specification made funny with functional programming: Haskell as a kind of formal method! Some concrete examples. Read more
After a few (17!) years spent designing and coding critical embedded and real time softwares, mainly for avionic systems, I came to the conclusion that most of the problems I had to cope with were not related to the complexity of the softwares. The first problem is often the way the specifications are written.
Writing softwares should be a very precise process, based on mathematics, to avoid misunderstandings. I guess that everybody agrees on writing specifications that are simple, practical, convenient, usable. Unfortunately this is sometimes not the case. Even worst, some specifications are informal, ambiguous and not verifiable.
Such specifications leads to buggy softwares, bugs discovered lately and long and expensive iterations.
My assumption is that formal specifications, even if they are a bit more expensive at the beginning, will lead to a better product and a more competitive process.
The goal of this book is to show how to formalize a specification and use this formalism to write safer code and better tests. The main idea is to find and identify bugs earlier within the specification, instead of waiting to see their side effects in integration stages.
There already exists a bunch a formal methods (B, event-B, TLA+, …). They all are very powerful but their usage is mastered by very few highly educated people on earth. Most engineers won’t use these methods in their every day work.
So which formalism could be a good compromise between power, expressiveness and simplicity?
A software is a function that takes input values and computes output values. These values are given by the user, measured by sensors or even computed by other softwares. If we assume that mathematical functions can represent softwares, we can write specifications (or models) with a high level language that remains close to the software implementation.
Using mathematical functions to specify or model a system has got several benefits:
- the model is formal and unambiguous: coders will understand it
- the model is executable by evaluating functions (it is deterministic, it is then easier to debug, it can be tested, test cases of the model can be reused to test the real implementation and prove that it conforms to the model)
- in some cases the model can be refined to get the final executable implementation
- using mathematics is a way to reduce the distance between the specification and the implementation
Some languages also have a good type system. If functions are strongly typed, the specification can be verified in some extend:
- a strong type system helps in detecting wrong interfaces between functions
- a static type system helps in detecting all type errors (whereas dynamic type systems only detects errors when the functions are evaluated and some errors may never be detected)
Functional programming languages are thus good candidates. For instance, Haskell and Ocaml are functional and have got a strong and static type system.
Haskell has a few more interesting characteristics. Lazy evaluation allows writing some data structures in a more natural way (e.g. infinite recursive data structures) without have to think about the evaluation order (as mathematical functions). Pure functions (i.e. functions with no side effects) are safer and easier to check.
I have then selected Haskell as a good candidate to model softwares or even complete systems with their environments.
So we will see how to write functional specifications with functional languages.
The advantage to writing functional specifications is that they can be executable. It means that they can be executed to:
- debug the model
- test and validate the model: the logic of the model can be checked before the real hardware target is ready
- animate a model and show a mock-up to you customer
Some kind of poor man formal method…
Executable test plans
The concept of executable specifications can be applied to tests!
Speaking about executable test plans is weird because the rationale of a test is to be executed to check something…
It should not be necessary to explicitly say “executable test plans”.
“Executable test plan” is not weird. It should be natural to everyone… But people often:
- write a test plan
- implement the tests
- execute the tests
- write a test report
- and make a lot of copy/paste mistakes because of such a long and boring process!
I will show in this book how easy it can be to achieve the same goal with functional test plans that are self-executable and that generate test reports themselves.
Plan of the book
The main goal is to show how Haskell (and functional programming in general) can be used as a multilevel formalization language:
- modeling / specification
And can be applied to different domains:
- real time embedded softwares
- generic purpose data processors (code generator, …)
I will quickly relate some stories of small bugs with big consequences that could have been avoided with functional specifications.
The book will start with a short introduction to functional programming. This introduction will be light because there are already a lot of tutorials and documentation on this topic.
The book will focus on the following points and their advantages:
- pure functional programming: why having no side effect is a good thing?
- strong static type system: how a type system can be used as a sort of formal system to describe a software?
Some applications: time formalization in real time systems
Reactive real time systems are often state machines. Their main activity is to modify their current state according to external stimuli.
Modeling such systems in a pure functional language (i.e. without any side effect) may seem impossible but we will see how to model time and its consequences on a reactive system.
This example will show the advantages of a pure functional language to describe states as well as to reason about their evolution in time.
- music generator from data measured by movement sensors
- formalism inspired by SCADE or Matlab Simulink and real time embedded softwares
Some applications: Arduino robot
Another model of reactive system will lead to a concrete realization: an Arduino robot able to sense its environment and react to some stimuli.
- formal specification in Haskell: reactions according to sensors (obstacle avoidance, moving toward a target)
- simulation of the robot in its environment (also simulated)
- actual coding using an Arduino platform
Modeling and Simulation
Modeling of a complete system: classical example of traffic lights and traffic in a road network.
- modeling of a traffic light (state machine, synchronization with its environment, …)
- modeling of a road-user (behavior, peak hours, commuting, MTBF of the vehicules, …)
- modeling of a road (maximal speed, …)
- global model (road network, users)
- graphic interface to visualize the simulation, interact, inject failures, …
Some applications: a well specified and tested calculator
This project is a rewriting of a calculator previously written in Lua by CDSoft. The idea is to recode this calculator in Haskell in a cleaner way:
- formal specification in Haskell
- strong typing: the type verification is some kind of formal method
- extreme usage of the compiler to detect more bugs and dead code
- complete unit tests
- non regression tests helps for future evolutions
- code coverage
Remark: I used this calculator in Lua (Calculadoira) daily. This new specification with its complete test suite helped me to find some bugs in the original implementation!
Some applications: ARINC 665 load generator
The ARINC 665 standard defines a loadable data format. This standard is widely used in aeronautics.
The generation of such loads is highly critical since they contain executables and data for embedded computers on aircrafts.
A functional specification can:
- reduce the distance between requirements and implementation (easier traceability)
- be tested in a simpler and safer way
The key idea is to describe requirements along with their properties to let the implementation be testable directly from the formalism of the requirements.
Risks and challenges
This project is a way to find opportunities to search and formalize different ways of specifying softwares.
Some aspects may not be easily worded in Haskell so the final content of the book may differ.
The goal is to find a good compromise between "formal Haskell specifications", "executable specifications", "executable test plans" and classical informal specifications.
- (30 days)