impress.js is not supported by your browser, sorry.

Functional specifications

Functional specifications

Christophe Delord ~

Sunday 28 February 2016

What’s wrong today?

The main problems in the everyday life of IT engineers are often the software specifications. The purpose of CDSoft FUN method is quite simple:

Specifications shall be:

but also:

  • simple
  • practical, convenient
  • usable
  • formal
  • unambiguous
  • verifiable
  • safe

Who am I?

I’m a software engineer. I’ve been working in the IT and aircraft industry for 17 years… writing softwares but not always in a clean and proper way:

So I have accumulated some ideas to make it differently.

I also have a passion for free software and sharing good ideas.

More about me:

Why this book?

This book is an opportunity to:

So I’ll be proud and happy if you decide to help me and fund a little bit this adventure.

I hope I can work part time and have more time for this project.

In return you will get a digital version of the book.

FUN answers

My point of view is that most of the software specifications - even for critical systems - are written:

Let’s see what’s wrong with this and what can be done to improve this situation…

Problem 1: ambiguous natural language

Natural language is nice

But critical (or not) softwares must be described unambiguously. Ambiguities lead to multiple and sometime inconsistent interpretations in practice.

Problem 1: ambiguous natural language

Problem 2: Close proprietary formats

You can not master a close proprietary format:

Proprietary formats are definitely the worst choice to write documents, especially if documents must be kept for a long time (e.g. 80 years in the aviation industry).

Problem 3: Inexploitable formats

Some formats - proprietary or not - are not suitable, especially office suite documents:

Problem 4: Unsafe office suites

Proposal 1: Formal language

Proposal 2: Open formats

Proposal 3: Open formats (again)

Proposal 4: Safe tools

To write text, you need a text editor:

Executable specifications

The advantage to writing functional specifications is that they can be executable. It means that they can be executed to:

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 plans

Executable test plan” is not weird. It should be natural to everyone… But people often:

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.


The next slides describe a provisional roadmap or plan for the book.

The main goal is to show how Haskell (and functional programming in general) can be used as a multilevel formalization language:

And can be applied to different domains:

Roadmap / Functional programming

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:

Roadmap / Some applications: time formalization in real time systems (1/2)

Reactive real time systems are often state machines. Their main activity is to modify their current state according to external stimuli.

Modelling 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 exemple will show the advantages of a pure functional language to describe states as well as to reason about their evolution in time.

Roadmap / Some applications: time formalization in real time systems (2/2)

Applications with real time models:

Roadmap / 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.

Roadmap / Modeling and Simulation

Modelling of a complete system: classical example of traffic lights and traffic in a road network.

Roadmap / 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:

Roadmap / 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:

The key idea is to describe requirements along with their properties to let the implementation be testable directly from the formalism of the requirements.

For who?

Whom is this book for?

This method has neither the power of formal methods like Event-B or tools such as Matlab Simulink or SCADE (yet?). Its advantages are:

It is therefore aimed at anyone looking for a nice combination of power, efficiency, simplicity and cost.

And now…

Your help is appreciated…

I think that crowdfunding is a solution:

Follow me