Tag - programmation

Entries feed - Comments feed

Last entries

Tue 17 Dec 2013

Book review: Better Embedded System Software

better_embedded_system_software_cover.gif Better Embedded System Software is a very good book if you write software, and not only embedded software!

I discover this book when following the Toyota Unintended Acceleration case where Philip Koopman, the author of this book, was a plaintiff's expert. Philip Koopman is an Associate Professor at the Carnegie Mellon University.

Why is this book so good? Because it explains in daily words what should be the ideal software development process. And not only it details the ideal process, but it gives concrete, down to earth advices on how to improve your current process and software development habits.

The book is divided into 30 small chapters, following the order of the usual V cycle (overall process, requirements and architecture, design, implementation, verification and validation, critical system properties). The chapters are very short, about 10 pages, and relatively independent. This one of the great point of the book: it is easy to read a chapter, there is not need to allocate a long time slot for it. You can pick the chapter that is most interesting to you. And as the chapters are right to the point, you immediately get useful advices and you can immediately start to apply them on your own development.

The other great quality of this book is that the author has a strong background in embedded software development. Therefore the advices are realistic and graduated. The author knows that you are going to find barriers and limitations in your work environment and he helps against them. For example, there are two chapters on producing some documentation but not too much. Even if you cannot apply the whole set of advices, you nonetheless get some ideas on own to improve your current software and what could be done in later steps.

I am not an expert on all the topics presented in this book (that's why I bought it!) but for the domains I knew (e.g. concurrent programming), the advices seem balanced and appropriate.

Of course, 10 pages for a chapter is very short and some subjects are so wide that they would deserve a book on their own (e.g. safety and security). In that case, Koopman's book give useful pointers to continue your reading and the summary he gives is an excellent introduction to the topic.

As I said many times, we are currently making very bad software and we should improve this situation. Better Embedded System Software is the one the very few books that you should keep close to your table and consult on a regular basis.

If you cannot afford the book, some quite detailed slides on Avoiding the 43 Top software risks have been made available by Philip Koopman.

Introduction aux méthodes formelles actualisée

Comme en 2010 et 2011, j'ai faire une intervention de 2h pour présenter les méthodes formelles à l'ESIR, école d'ingénieur de Rennes 1. J'ai un peu actualisé la présentation, je pense qu'elle est plus illustrée et j'ai introduit quelques démonstrations d'utilisation des outils. La présentation est disponible en PDF ou en source au format PowerPoint (licence Art Libre, sauf pour les illustrations, que j'ai pioché à droite et à gauche sur le web).

Note pour les libristes : la plupart des logiciels mentionnées sont libres.

Fri 02 Dec 2011

A draft of library to handle physical units in OCaml

When writing a computer program that interact or handle with the physical word, a common need is to manipulate physical units like meter, second or km/h. Most of the time it is up to the programmer to ensure that the physical units are correctly used, even if there are rules to check them (divide only meters by meters, ...). All physicists are routinely checking their equations with those rules. Why not programmers?

So here is a draft of OCaml library to do just that: computations on physical values while ensuring physical units rules are followed (for example, you only add meters to meters, not meters to seconds). Here are the SIunits.mli and SIunits.ml files.

The use of the library are quite simple:

  • A set of functions to create values with units from simple floats. For example meter 1.0 (or simply m 1.0) creates a value containing 1 meter;
  • A set of utility functions to handle SI prefixes like kilo, to normalize a value (i.e. to remove the scaling factor) or to print it with its units. For example, to enter a length of 160 km one would write kilo (m 160.0);
  • A set of four operators, +!, -!, *! and /! to do basic computations on those values. For example, to enter a speed of 160 km/h, one would use let speed = (kilo (m 160.0)) /! (hour 1.0). To compute the distance travelled at previous speed during 120 s, one would do let distance = (normalize_si_value speed) *! (s 120.0) and the program can print 5333.333333 .m;

Internally, I have followed the proposal of "Checking SCADE Models for Correct Usage of Physical Units" paper by using a vector of 8 units: 7 base units (following those defined in the SI system) plus one power of 10 unit for the scaling factor (to handle kilo, mega or more exotic units like hour). In fact, to be really exhaustive one would need some additional units but the current code is really a draft. Then, the rule for addition or subtraction is to check that the units are identical, while for multiplication and division the units of the two numbers are added or subtracted. See the above paper for details.

There is a lot of work to transform this draft code into a real, usable and exhaustive, library:

  • Power and root operators;
  • Comparison operators;
  • Decision operators;
  • Dimensionless units;
  • Absolute or relative values;
  • More prefixes and exotic units;
  • And of course of lot of tests for above code.

Right now, I do not intend to extend the current code but if other people are interested, I could work on it and open an OCaml Forge project. If there is a need, let me know.

And now a question for the OCaml experts: would it be possible to replace the dynamic checks currently implemented in this library by static checks using OCaml type system (for example using Phantom types)? I think this is not possible: the base units are like arrays of the same size, you need a more expressive type system to express constraints on them (like Coq's Dependent types). But I would be pleased to be shown wrong. :-)

Track artifacts of a project: the Qualifying Machine

In a recent blog post about literate programming tools, I advocated for tools that would allow programmers to track changes in a set of documents, source code, figures, test suites, etc. that makes a software. More exactly, I was saying:

Moreover, to really exploit the full potential of literate programming, one needs to produce and track dependencies between several documents. For example, if I modify the specification, I need to modify some parts of the code. Inversely, if I change my code I need to know which part of the "specification" have to be updated. This tracking between pieces of code/documentation goes to test, user documentation, code documentation, test review, Q&A documents, GUI design, mathematical scripts describing an algorithm, formal models to check the software, etc. And more importantly, if I modify a piece of this code/documentation, I need a list of all document parts I need to review and possibly update, a kind of make on steroids.

I was also saying:

Overall, one needs an integrated documentation system that is able to encompass all the kind of artefacts that make a software and that can be used to maintain those artefacts along the whole life of the software, from design to maintenance. And this system should be flexible enough to not constrain you to a fixed development environment, letting you chose the tools that you prefer.

It appears that others have the same ideas as me (as usual ;-). Recently Matteo Bordin presented the Qualifying Machine that encompasses some of those ideas.

The Qualifying Machine main idea is to provide a development environment for avionic software where one could do continuous qualification. When you modify an artifact (source code, specification document, etc.), the tool tracks all the implied changes on other artifacts and let you know what kind of action you need to do to re-qualify your software (tests to execute, formal proofs to do, etc.).

I let you look at Matteo's presentation on Agile Qualification and the Qualifying Machine to understand its details. The Qualifying Machine is currently just a few ideas with a small prototype for GnatCheck but it sounds quite interesting.

Thu 30 Jul 2009

Critique livre : La programmation en pratique

La programmation en pratique Un livre que je recommande chaudement à tout programmeur ou apprenti programmeur : La programmation en pratique de Brian W. Kernighan[1] et Rob Pike, éditions Vuibert informatique, ISBN 2-7117-8670-6.

Ce livre aborde tous les sujets qu'un bon programmeur doit connaître :

  1. Le style : comment écrire du code clair et bien commenté ;
  2. Les algorithmes et structure de données : l'importance de choisir un bon algorithme, évaluer sa complexité et les différents types de structures de données (listes, arbres, tables de hachage) ;
  3. La conception et l'implémentation : comment concevoir un programme, choisir un algorithme et bien réutiliser les bibliothèques existantes ;
  4. Les interfaces : comment faire un code réutilisable par d'autres ;
  5. Le débogage : quelles méthodes et outils utiliser pour trouver les erreurs de ce !!#@!?!! de programme ;
  6. Les tests : comment tester son programme, de manière systématique et reproductible ;
  7. Les performances : comment évaluer les goulots d'étranglement dans un programme et comment y remédier ;
  8. La portabilité : comment écrire un programme exécutable sur différentes plate-formes, et ce même en langage C ! ;-)
  9. La notation : quelques exemples qui montrent qu'un programme utilisant une notation adaptée facilite la vie de son utilisateur.

Ce livre est abondamment illustré d'exemples en C, C++, Java, Perl ou Awk. Les exemples sont clairs et l'approche est pragmatique, mais avec le soupçon de théorie quand c'est nécessaire. Chaque chapitre se termine par des exemples et des lectures complémentaires, permettant d'approfondir un sujet si nécessaire. Les auteurs ont de l'expérience et savent transmettre leur savoir.

J'ai particulièrement aimé ce livre car il concentre dans un ouvrage relativement concis (300 pages) tous les conseils que j'ai pu lire ou découvrir à droite et à gauche dans ma vie de programmeur. Et même si vous programmez en PHP, Python ou OCaml, les points abordés sont universels et valides pour tous les langages. Ce livre est une perle, lisez-le... et appliquez ses règles ! ;-)


[1] Oui, LE Kernighan du langage C et de Awk.