The validation in the early steps of the development process

The validation in the early steps of the development process

Imen Sayar Jeanine Souquières 

LORIA – CNRS UMR 7503 – Université de Lorraine Campus Scientifique BP 239, 54506 Vandoeuvre lès Nancy cedex, France

Corresponding Author Email: 
{Firstname.Lastname}@loria.fr
Page: 
11-41
|
DOI: 
https://doi.org/10.3166/ISI.22.4.11-41
Received: 
|
Accepted: 
|
Published: 
31 August 2017
| Citation
Abstract: 

Improving the quality of a system begins by the requirements elicitation. Our goal is to take into account the validation since the understanding of the requirements and all along the development of their Event-B specification. Our challenge is to bridge the gap between requirements, those of the client, and the specification, that of the computer scientist. We make explicit the interactions between the requirements and the specification under construction. The validation is studied for formal models with regard to the requirements. The verification may detect incoherences and contradictions in both requirements and formal specification. The Rodin platform tools are important all along the development to improve the quality and the documentation of the system. Rodin and the ProR plugin allow us to manage the trace of the requirements and their specification. The documentation and the feedback of the different used tools for the validation and verification are available at any time of the development. We illustrate our approach to the case study of an aircraft landing system. 

Keywords: 

requirements, specification, refinement, validation, verification, tools

1. Introduction

Le travail de recherche sur l’ingénierie des exigences présenté dans (van Lamsweerde, 2008) insiste sur deux activités à résoudre : l’analyse du domaine et la modélisation des exigences. Le groupe Standish a conduit des études par l’interview d’entreprises dans  le  domaine  du  logiciel.  Il  a  récemment publié  une  dernière version du Rapport CHAOS dont le premier date de 19941 ; l’une des principales causes des difficultés dans le développement de systèmes réside dans la prise en compte des exigences. Celles-ci sont souvent très pauvres, voire inexistantes.

Depuis 1998, Abrial (Abrial, 1998) propose des bases pour la rédaction de la spécification. Un premier texte explicatif se consacre à l’exposé des besoins. Il s’intéresse au pourquoi ou à sa compréhension. Ce document peut être oublié lorsqu’il n’apporte plus de nouvelles informations. Le deuxième texte appelé texte de référence du futur système expose les connaissances nécessaires à la réalisation du futur système. Ces deux textes peuvent contenir des redondances.

Le processus de développement de systèmes à l’aide du raffinement utilisé dans Event-B (Abrial, 2010) est comparable au processus de la cascade. Le modèle initial précise  son  invariant  que  le  système  doit  garantir  et  chaque  raffinement est  à nouveau prouvé par son invariant. Cette approche assume les propriétés suivantes :

– les exigences sont explicitées pour décrire le modèle initial ;

– le  modèle initial est  une  description formelle répondant aux exigences de sécurité et fonctionnelles et ;

– les décisions prises lors d’un raffinement sont mémorisées en liaison avec les exigences associées.

En réalité, peu de développements décrivent entièrement ces propriétés. Les exigences  évoluent  avec  le  développement,  celles-ci  ne  sont  pas  forcément exprimées  dans  le  modèle  initial,  de  nombreux  raffinements  introduisent  de nouvelles informations dans le modèle (Abrial, 2006).

Les activités de validation et de vérification sont utilisées dans les premières étapes du développement depuis les exigences jusqu’à la spécification formelle. Parmi les techniques de validation de modèles, leur exécution est plus attrayante, particulièrement dans le cadre de la modélisation à base de modèles Event-B. La plus grande difficulté vient du non-déterminisme de la plupart des modèles raffinés. En fait, il est recommandé de réduire l’abstraction et le non-déterminisme pas-à-pas. Tandis que des outils actuels, tels que ProB (Leuschel et al., 2003, 2008), peuvent animer des modèles avec un non-déterminisme modéré, ils ne peuvent pas toujours traiter l’ensemble des problèmes soulevés. Des stratégies d’exploration exhaustives tombent rapidement dans l’explosion combinatoire.

1. Rapport CHAOS du Standish Group (http ://www.standishgroup.com).

Dans notre approche, nous mémorisons le cahier des charges, nous prenons en compte ses différentes mises à jour et nous explicitons sa place dans le processus de développement (Abrial, 2009). Pour cela, un ensemble de liens, ou relations, entre exigences et spécifications a été identifié et réalisé avec la plateforme Rodin (Abrial et al., 2010) et le plugin ProR (Jastram, 2010). Ces liens sont mis à jour tout au long du   processus  du   développement,  depuis   le   cahier   des   charges  jusqu’à   sa spécification terminée. Différentes actions entre l’évolution de ces deux « mondes » sont présentées (Sayar et al., 2016). Le choix d’un ou plusieurs besoins nous amène à la spécification en cours de développement. Depuis la spécification, les actions modifiant les exigences permettent :

– d’ajouter des termes formels dans une exigence,

– d’ajouter, supprimer et mettre à jour une exigence,

– de valider et vérifier la spécification vis-à-vis des exigences à l’aide des outils disponibles. Ces outils permettent de découvrir des incohérences et des imprécisions aussi bien dans la spécification en cours que dans les besoins.

La spécification est en cours de développement et décrite pas à pas. L’ensemble des outils disponibles, tels que les outils de validation et de vérification, sont utilisés tout au long de ce développement, et non seulement lorsque la spécification est terminée. Dans ce papier, nous nous intéressons plus particulièrement à l’activité de validation en tant que processus rigoureux. Cette activité démarre avec la structuration des besoins, avant que la spécification associée ne soit introduite, jusqu’à l’animation des modèles Event-B. Ces modèles sont validés relativement aux besoins du client, en vue de détecter des problèmes.

Dans la suite de cet article, la partie 2 présente brièvement la méthode Event-B et la plateforme Rodin. Nous utilisons les outils suivants : ProR pour gérer les besoins informels en lien avec la spécification en Event-B, les outils de vérification, de validation et Event-B Statemachine. La partie 3 présente notre approche en termes du cahier des charges et de sa spécification en cours de développement. La partie 4 concerne la préparation de la validation dès la première étape du processus de développement, celle de l’expression de ses exigences en langage naturel. La partie

5 concerne l’application de notre approche à une étude de cas. Nous présentons quelques étapes de développement depuis les besoins jusqu’à la spécification en Event-B. La validation est abordée dans la partie 6 en vue de prouver la correction de la spécification relativement aux besoins à tout moment du développement. La partie 7 aborde la détection d’incohérences dans les exigences en liaison avec la vérification. Les travaux connexes sont présentés dans la partie 8. Une conclusion est proposée dans la partie 9 avec nos travaux futurs.

Notre approche est illustrée par l’étude de cas d’un système de contrôle du train d’atterrissage d’un avion (Boniol et al., 2014). Son architecture est présentée dans la figure 1. Il s’agit d’un système hybride combinant :

– une partie mécanique et hydraulique actionnée par des électrovannes et observée par des capteurs. Elle contient trois ensembles d’atterrissage,

– une partie digitale incluant le logiciel de commandes et,

– l’interface de contrôle pour le pilote.

Figure 1. Architecture globale

 

2. Cadre formel et outils support
3. Présentation de notre approche
4. Préparation à la validation
5. Application de notre approche
6. Validation
7. Vérification
8. Travaux connexes
9. Conclusion et perspectives
  References

Abrial J.-R. (1998). Le Cahier des Charges: Contenu, Forme et Analyse (en vue de la Formalisation), Technical report, Connsultant.

Abrial J.-R. (2003). B : passé, présent, futur. Technique et Science Informatiques, vol. 22, n° 1, p. 89-118.

Abrial J.-R. (2006). Formal Methods in Industry : Achievements, Problems, Future. 28th International Conference on Software Engineering, Shanghai, L. J. Osterweil, H. D. Rombach, M. L. Soffa (Eds), China, ACM, p. 761-768.

Abrial J.-R. (2009). Faultless Systems: Yes We Can! IEEE Computer, vol. 42, n° 9, p. 30-36.

Abrial J.-R. (2010). Modeling in Event-B: System and Software Engineering, Cambridge University Press.

Abrial J.-R., Butler M. J., Hallerstede S., Hoang T. S., Mehta F., Voisin L. ( 2010). Rodin: An open toolset for modelling and reasoning in Event-B. STTT, vol. 12, n° 6, p. 447-466.

Alkhammash E., Butler M., Fathabadi A. S., Cirstea C. (2015). Building Traceable Event-B Models from Requirements. Science of Computer Programming (Special Issue on Automated Verification of Critical Systems, AvoCS’13), vol. 111, Part 2, p. 318-338.

Bendisposto J., Leuschel M., Ligot O., Samia M. (2008). La validation de modèles Event-B avec le plugin ProB pour RODIN. Technique et Science Informatiques, vol. 27, n° 8, p. 1065-1084.

Boniol F., Wiels V. (2014). Landing Gear System case Study. ABZ Case Study, Berlin, Communications in Computer and Information Science, Springer, vol. 433, p. 1-18.

Driss S. (2014). From natural language specifications to formal specifications via an ontology as a pivot model, Theses, Université Paris Sud - Paris XI, June.

Gamma E., Helm R., Johnson R., Vlissides J. (1995). Design Patterns : Elements of Reusable Object- oriented Software, Addison-Wesley Longman Publishing Co., Inc., Boston, USA,

Gunter C. A., Gunter E. L., Jackson M., Zave P. (2000). A Reference Model for Requirements and Specifications - Extended Abstract. Proceedings of the 4th

International Conference on Requirements Engineering, IEEE Software, p. 37-43.

Hallerstede S., Jastram M., Ladenberger L. (2014). A Method and Tool for Tracing Requirements into Specifications. Sciences Computer Program, vol. 82, p. 2-21.

Hallerstede S., Leuschel M., Plagge D. (2011). Validation of Formal Models by Refinement Animation. Sci. Comput. Program., vol. 78, n° 3, p. 272-292.

Heisel M.. Souquieres J. (1999). A Method for Requirements Elicitation and Formal Specification. Proc. 18th Int. Conference on Conceptual Modeling. ER’99. n° 1728 in LNCS Springer-Verlag, p. 309-324.

Hoang T. S., Fürst A., Abrial J. (2013). Event-B Patterns and their Tool Support. Software and System Modeling, vol. 12, n° 2, p. 229-244.

Hoare C. A. R. (1969). An Axiomatic Basis for Computer Programming. Commun. ACM, vol. 12, n° 10, p. 576-580 & 583.

Jacquot J. (2015). Premières leçons sur la spécification d’un train d’atterrissage en B Événementiel. Technique et Science Informatiques, vol. 34, n° 5, p. 549-573.

Jastram M. (2010). ProR, an Open Source Platform for Requirements Engineering based RIF. SEISCONF.

Leuschel M., Butler M. (2008). ProB : an Automated Analysis Toolset for the B Method. International Journal on Software Tools for Technology Transfer, vol. 10, n° 2, p. 185-203.

Leuschel M., Butler M. J. (2003). ProB: A Model Checker for B. FME 2003: Formal Methods, International Symposium of Formal Methods Europe, Pisa, Italy, Proceedings, p. 855-874.

Mashkoor A. (2016). The Hemodialysis Machine Case Study. Abstract State Machines, Alloy, B, TLA, VDM, and Z. 5th International Conference, ABZ 2016, Linz, Austria, May 23-27, Proceedings, p. 329-343.

Mashkoor A., Jacquot J.-P. (2016a). Validation of Formal Specifications through Transformation and Animation. Requirements Engineering, Springer Verlag.

Mashkoor A., Yang F., Jacquot J.-P. (2016b). Refinement-based Validation of Event-B Specifications. Software and Systems Modeling, Springer Verlag.

Ponsard C., Darimont R., Michot A. (2015). Combining Models, Diagrams and Tables for Efficient Requirements Engineering: Lessons Learned from the Industry. Actes du XXXIIIe Congrès INFORSID, Biarritz, France, May 26-29, p. 235-250.

Sayar I., Souquières J. (2016). La validation dans le processus de développement. 34e Congrès INFORSID, Grenoble, France.

Sayar I., Souquières J. (2017). Du cahier des charges à sa spécification. 16e journées AFADL, 13 au 16 Juin 2017, Montpellier, France.

Su W., Abrial J.-R., Huang R., Zhu H. (2011). From Requirements to Development : Methodology and Example. 13th International Conference on Formal Engineering Methods, Durham, UK, p. 437-455.

Su W., Abrial J.-R., Zhu H., (2014). Formalizing hybrid systems with Event-B and the Rodin Platform. Sci. Comput. Program, vol. 94, p. 164-202.

van Lamsweerde A. (2008). Requirements Engineering: from Craft to Discipline. Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of Software Engineering, Atlanta, Georgia, USA, p. 238-249.

van Lamsweerde A. (2009). Requirements Engineering - From System Goals to UML Models to Software Specifications, Wiley.

Yang F., Jacquot J. (2011). An Event-B Plug-in for Creating Deadlock-Freeness Theorems, 14th Brazilian Symposium on Formal Methods, Brazilian Computer Society.