Méthodes formelles et entreprises [fermé]

Question

Alors ...

J'enseigne les méthodes formelles en génie logiciel. J'enseigne également des "méthodologies agiles". La plupart des gens semblent penser que c'est contradictoire. Je pense que cela a beaucoup de sens ... Je travaille aussi pour une entreprise, où nous devons réellement faire avancer les choses :) Bien que je puisse appliquer les points de compétence que je me suis acquis à la "spécification". Au quotidien, mes collègues fuient généralement le mot "formel".

J'avais l'habitude de penser que cela était dû à la manière intrinsèque dont nous apprenons à programmer: nous sommes généralement motivés pour trouver une solution qui fonctionne, et non pour comprendre le problème. Ensuite, j'ai pensé que cela était dû au fait que la plupart des gens de la communauté formelle ne sont pas des ingénieurs, mais des mathématiciens ou des informaticiens. De nos jours, je me demande si c'est juste parce que la communauté des méthodes formelles se cache derrière une sorte de "obscurcissement". loi à utiliser tous les symboles UNICODE disponibles, à développer activement des outils grossiers et non esthétiques et à rire face aux normes.

Oui, je suis passé d'un message "les blâmer". à un "nous blâmer" & perspective ;-)

Ma question est donc la suivante: utilisez-vous des méthodes formelles dans votre entreprise? Les avez-vous présentés ou s'agissait-il de conditions préalables? Quelles techniques utilisez-vous pour dissiper le chaos des mathématiques et les inciter à utiliser des méthodes formelles? Que pensez-vous des outils actuels qui manquent pour un usage plus général?

Answer 1

Pour convaincre les gens d’adhérer à toutes les méthodes ou méthodologies , vous devez leur montrer comment résoudre les problèmes qu’ils rencontrent. S'ils peuvent le voir améliorer leur vie, leurs chances de les faire adopter seront beaucoup plus grands.

Et si vous ne pouvez pas leur montrer cela, vous vouliez peut-être adopter des méthodes fondées sur la philosophie plutôt que sur l'aspect pratique. À moins que les autres partagent votre philosophie, vous n'irez nulle part. Et peut-être que vous ne devriez pas.

Au fil des décennies, de nombreuses méthodologies ont été utilisées. Les plus récents répondent toujours aux lacunes des anciens, mais les projets échouent toujours. Pourquoi? Parce que les stars du rock qui proposent de nouvelles méthodologies sont des stars du rock et ont créé une nouvelle méthodologie précisément parce qu'elles comprennent les problèmes sous-jacents et comment les appliquer. Ceux qui viennent après ont tendance à suivre aveuglément la recette, et ça ne marche pas très bien.

Donc, je pense que la meilleure chose à faire est d’enseigner les problèmes sous-jacents, puis de montrer comment diverses méthodes tentent de les résoudre. Les différences au niveau des entreprises, des projets et des équipes sont si grandes qu'aucune méthodologie ne peut être appliquée avec succès à toutes les combinaisons. Apprendre à choisir un outil approprié et à bien l’appliquer est crucial.

Answer 2

Merci pour toutes vos contributions. Ils sont très perspicaces. Permettez-moi de brûler un peu (ne le prenez pas personnellement, cependant: -)

La plupart des gens semblent penser que les méthodes officielles ne concernent que la vérification de programme. Ou des systèmes critiques. C’est peut-être vrai si nous poursuivons le cliché ultime: prouver que nous exécutons correctement le programme (vs.s. validation, qui demande, comme l’a dit un contributeur, si nous réalisons le bon programme).

Mais considérez les outils de recherche / vérification de modèles, tels que Alloy. Apprendre à utiliser un outil comme celui-ci prend un temps négligeable à quiconque est habitué à UML et à OO. Néanmoins, cela peut vous donner un aperçu immédiat de votre modèle. Il ne faut généralement pas plus de 10 minutes pour trouver un contre-exemple sur un sous-ensemble suffisamment petit du modèle que l'on essaie d'utiliser (et cela inclut la description du modèle dans Alloy en premier lieu).

Prenons l'exemple de l'ingénierie des exigences. On dessine généralement beaucoup d’UML. Cependant, peu de personnes utilisent OCL et de nombreuses règles métier sont annotées de manière informelle en langage naturel. Pourquoi? Des contraintes de temps?

Considérons maintenant le fait que la majorité utilise simplement son instinct pour prouver qu'un modèle est satisfaisable. Encore une fois, pourquoi? Je peux prendre le même temps (probablement même moins, car je n’ai pas besoin de me soucier de dessiner l’esthétique) pour écrire ce modèle dans Alloy, et juste vérifier sa satisfiabilité? Et de quel genre de mathématiques ai-je besoin maintenant? "Prédicats"? Nom de fantaisie pour les IF et les booléens ;-) Quantificateurs? Noms de fantaisie pour ForEachs () ...

Qu'en est-il des grands systèmes d'information? Ils n'ont pas besoin d'être critiques ... Essayez simplement d'analyser dans votre tête un diagramme conceptuel (pas d'implémentation!) Avec plus de 600 classes. Je vois beaucoup de gens se cogner la tête contre le mur avec des erreurs de modèle faciles à commettre parce qu'ils ont manqué une contrainte ou que le modèle permet que des choses stupides se produisent.

Le fait est qu’il n’est pas nécessaire d’utiliser des approches formelles de la tête aux pieds. Certes, je pourrais prouver une application entière en Coq et certifier qu’elle est conforme à 100% à certaines spécifications. Ce peut être l'approche Informaticien / Mathématicien.

Malgré tout, avec une philisophie GTD, pourquoi ne puis-je pas déléguer certaines tâches à l'ordinateur et lui permettre d'améliorer mon développement? Est-ce vraiment une question de "temps", ou simplement, de manque de capacités techniques et de volonté d'apprendre / d'innover?

Answer 3

Travailler avec les secteurs d'activité Le développement informatique dans une entreprise implique de transférer les connaissances sur les affaires des hommes d'affaires aux responsables des développeurs. Même si je trouve moi-même que les mathématiques abstraites sont l'un des plus grands passe-temps, c'est un outil de communication épouvantable. Et la communication est ce dont il s'agit. Il est certes concevable que je réussisse à convaincre les informaticiens d’adopter des notations plus abstraites, mais je n’ai fondamentalement aucune chance avec les gens d’affaires.

Bien que, dans certains domaines, les méthodes formelles puissent jouer un rôle dans une entreprise (logiciels spécialisés lourds en mathématiques et en logique, besoin important de propriétés vérifiables comme dans les logiciels critiques pour la sécurité), elles fournissent peu d'aide pour obtenir les exigences correctes. par exemple comment exécuter un ordre client en émettant un ou plusieurs ordres d'approvisionnement à un ensemble de fournisseurs externes ou internes possibles.

Je pense que le jury n’est toujours pas au courant des approches basées sur des modèles et des langages spécifiques à des domaines Je pense qu'ils réussiront ou échoueront, selon qu'ils répondent plus rapidement des souhaits et des besoins de l'entreprise du point de vue informatique et qu'ils supposent que les hommes d'affaires devront effectuer des études approfondies.

La technologie est facile. La communication est difficile. Les méthodes formelles peuvent nous aider à bien faire les choses, mais celles que j'ai vues ne font rien pour nous aider à faire les bonnes choses. (Oui, ce sont des clichés, mais c'est parce qu'ils sont inévitablement et douloureusement vrais.)

Answer 4

Je suis un cours sur la spécification et la vérification. Dans le cadre de la structure du cours, nous procédons comme suit: 1. Outils d’apprentissage comme PVS (Prototype Verification System) http://pvs.csl.sri.com/ et SMV (modélisation et vérification de logiciels) http: //www.cs.cmu .edu / ~ modelcheck / smv.html 2. En dehors de cela, nous disséquons les accidents dus à des pannes de logiciels. Par exemple - Echec d’Ariane V

Je pense que les méthodes formelles sont plus applicables aux scénarios dans lesquels le coût de l'échec est supérieur au coût de conception. Et il semble apte à les utiliser pour les logiciels utilisés dans des systèmes critiques. J'imagine qu'il est utilisé dans l'avionique, la conception de puces, etc., et que l'industrie automobile actuelle le met également en pratique.

Answer 5

J'ai essayé d'amener les gens à adopter des méthodes de spécification formelles à plusieurs reprises (Z et Alloy) et j'ai fait la même expérience que la vôtre: La plupart des gens, bien qu'ils se sentent utiles, sont très mal à l'aise de les utiliser pour travail effectif.

Assez drôle, les mêmes personnes sont plus qu'heureux de produire des diagrammes UML totalement inutiles en quantités considérables.

Je pense qu'il y a deux raisons principales à cela:

a.) De nombreux développeurs ne sont pas à l'aise avec le niveau d'abstraction requis par une approche formelle. Le fait que la plupart des études de mathématiques de niveau débutant concerne uniquement le calcul et que les mathématiques non discrètes peuvent en faire quelque chose.

b.) Les méthodes formelles requièrent une approche de conception très ascendante, dans laquelle vous concevez votre modèle principal à partir du sol et le rendez étanche à l'air, puis vous le connectez aux besoins réels des utilisateurs en leur fournissant une interface. Comme nous avons tendance à imposer des exigences aux efforts de développement, une approche descendante semble plus naturelle, même si elle conduit souvent à des modèles incohérents. C'est comme réaménager un sous-sol sous votre maison après sa construction.

Answer 6

Les méthodes formelles n’ont aucun sens dans les systèmes où le coût d’une défaillance est faible.

Dans une application Web de production, vous disposez de plusieurs boîtiers frontaux, plusieurs boîtiers principaux, plusieurs boites de bases de données. Si un programme échoue sur l'un d'entre eux, il s'agit d'un non-événement. Le matériel est tellement bon marché que vous pouvez construire ces systèmes à un prix bien inférieur au coût de spécification formelle de tous vos logiciels.