Un futur codeur Scade ;) Je peux te dire que la verif formel de scade débute.
Et je peux te dire que dans la vrai vie, j'ai pas eu vent de comment cela passe; je le fais tous les jours. Je dois respecté la DO178B (celle d'aujourd'hui, en 1970, elle n'existait pas).
Dans ce que tu décris, je ne vois rien de différent avec un test utilisant un "golden model", que l'on utilise en ce moment.
Si tu as une autre méthode moins chiante, je suis preneur.
Si c'est pas prouvé, il te donne un contre exemple immédiatement, donc tu corriges très rapidement ton appli pas besoin de la suite de non régression "overnight". C'est sans doute la partie la plus utile.
Si c'est prouvé bingo. Si l'assertion est correctement exprimé. C'est en fait moins utile que le cas précédent.
Si il n'y arrive pas, le prouveur d'Esterel te donne une profondeur temporel genre 10 coups d'horloges, si on connait la structure de son code (pas de mémoire à plus de 10 coups en arrière), on peut être confiant.
Dans la vérification formel, j'inclus aussi la génération automatique de vecteurs d'entrée pour augmenter le taux de couverture. Il n'y a plus qu'à avoir des sorties de références ou des assertions à vérifier.
Le static timing analyser de temps en pire cas permet de te trouver ton pire cas en timing. (il faut par contre un beau modèle de ton systèm)
Et bossant pour une boite qui vend un "langage formel" pour ce genre d'application, je peux te dire que tout ce qui est vérification formel est loin d'être la règle, et est encore moins reconnu (sauf peut-être dans le ferroviaire et encore).
"La spécialités de mes formateurs en test de logiciels" et ils forment à quel genre de technique ?
J'ai l'impression qu'il y une différence entre les pratiques habituelles pour le développement live critical et ce que tu crois l'être... vu depuis un labo.
Les tests de performance et d'endurance vont te permettre d'obtenir un degré de confiance en mesurant le temps de réponse.
Si tu joues le jeu de la vérification formelle, tu démonteras juste que ce n'est pas prouvable. T'es bien avancé.
Renseignes toi mieux. Ce genre d'outil existe déjà et fonctionne.
En général, tu fais un test pour couvrir un point de spécification. Donc, tu trouves à la main des vecteurs d'entrée, tu évalue ce que doivent être tes sorties et tu compares avec la sortie de ton code.
Dans la preuve formel, tu ajoutes une assertion qui correspond à un point de spécification. La vérification formel balaye toutes les possibilités d'entrée à la recherche d'un contre exemple.
Dans le cas du test, tu es limité par les vecteurs d'entrée que tu trouves à la main alors qu'avec un moteur de preuve, tu as l'exhaustivité.
Tu as perdu la possibilité de prouver quoique ce soit, puisque sur un OS non temps-réel tu n'as strictement aucune garantie sur la disponibilité des ressources.
Quelle différence entre une vérification formelle et un test, ici ?
C'est pas parcque tu as réussi à formaliser les specs que les specs sont valides.
C'est évident ça. mais dans ce cas, on parle de valider la spec par celle au dessus. Au moins on peut trouver les incohérences.
Et là si tu fais pas des tests d'ergonomie...
Cela veut dire que tu codes en suivant une spec mais que tu tests en suivant autre choses ? Je te souhaite bien du courage pour expliquer d'où vient le problème à ton client ! (sa spec et pas ton code)
'est con mais c'est comme ca dans la vraie vie, souvent tu te buttes face à un client qui ne veut pas répondre (pas le temps ou ne sais pas trancher) et tu dois faire des choix.
Je commençais à comprendre que ton client ne faisait pas des avions :)
Pour le dsp, c'est moyennement gênant, TI fournit des codecs mpeg4 avec la puce. Pour la carte graphique malheureusement...
Peut-être que la 3D du snapdragon de qualcomm est plus ouverte. La pversion la plus puissante a une puce avec l'équivalent de 2 cortex A8 à 1.5ghz avec une puissance de calcul en SIMD double (Qualcomm a fait sa propre version de l'architecture ARMV7). http://www.hardmicro-fr.net/news-article.storyid-3422.htm
Il y en a avec plus de 5h d'autonomie réel mais il dépasse le kg.
La qualité du clavier va rendre le produit intéressant ou pas, j'aurais aimer un écran 10" en 720p mais si le clavier fait mal au doigts c'est encore pire.
Tu as perdu quoi ? Dire que tu compares une méthode formelle (style celle de absint qui utilise un modèle cpu+mémoire) avec la simple mesure de quelques vecteur d'entrés !
Personne n'a dit que les tests offraient de garanties.
Pourquoi tu sous entends que la solution formelle serait moins bonne alors ?
Un valideur formelle ne valide pas les specs, d'où l'intérêt de mon exemple qui n'a strictement rien de fallacieux, et qui au contraire me paraît très réaliste.
Bien sur qu'elle valide les specs ! En rédigeant la spec formelle tu identifies immédiatement tous les manques et précision à demander à ton client !
Un outil formel pour le faire permettrait de te trouver le ou les vecteurs d'entrées correspondant à ton pire cas et mesurer ensuite le temps d'exécution. Tout cela pourrait être automatique.
Il n'y a pas à tortiller, si la "spec" est "le programme termine sur l'entrée 16 en temps 64", c'est trivial, si c'est "le programme calcule factorielle", c'est indécidable. Les specs que tu veux vérifier, c'est parce qu'elles sont non triviales,
Non, c'est aussi parce que le programme est gros.
Tu veux vérifier que tu ne t'es pas planté dans la copie d'une équation, dans la recopie d'une constante, que tu n'as pas de cas ou tu core dump.
"le programme calcule factorielle"
Sauf que ta spec ne dira pas ça. Il dira factoriel selon l'algo bidule précis à 10^-14 en code double flottant. De toute façon, je vois mal factoriel comme étant une fonction de base de ton logiciel de preuve.
La "preuve" sera l'équivalence à x^-14 prêt entre l'équation mathématique de la spec et ton code (souvent des développements limité).
Mais pour le cas de factoriel, le test tel que définit par la DO-178B demande de couvrir les classes d'équivalences, ce qui va se réduire à tester un nombre négatif, zéro, un nombre positif, voir les nombres max et min du range spécifié, et le range+1 pour voir que cela ne plante pas. 7 tests en tout pour vérifier l'équivalence à 10^-14 prêt et pour avoir la certif de ton avion.
Si tu fais quelques milliers de test en random() en plus, c'est encore mieux (mais la certif s'en fout). Les partitions par classe d'équivalence fonctionnent en test boite blanche quand tu connais la tête du code et que tu voix bien qu'il n'y a pas de branchement. De toute façon, à l'exécution du test, tu vérifies la couverture de code.
Certe tu n'auras pas prouver l'équivalence entre spec et code mais tu auras une grande confiance, ce qui est le principale.
Je rajouterai l'équivalence des programmes, c'est énorme pour l'optimisation.
Je ne pense pas que l'on est besoin que toutes assertions soit prouvable, j'ai peur que cela sois compliqué. Je préfère que des assertions simples (division par zéro) puisse être traité sur le programme en entier. Générer un contre exemple, c'est indispensable tellement, c'est utile.
La génération automatique de pattern de teste pour passer les assertion en dynamique pour faire la couverture de code est très utile (pour avoir le pire cas en timing aussi). Les stratégies de tests pour trouver les vecteurs sont parfaitement automatisable (gestion des classes d'équivalence, branches, valeur singulière, etc..)
[^] # Re: prouveur automatique/assistant de preuve
Posté par Nicolas Boulay (site web personnel) . En réponse au journal La preuve de programme : où en est-on ?. Évalué à 2.
"La première sécurité est la liberté"
[^] # Re: Se passer des tests ...
Posté par Nicolas Boulay (site web personnel) . En réponse au journal La preuve de programme : où en est-on ?. Évalué à 3.
Et je peux te dire que dans la vrai vie, j'ai pas eu vent de comment cela passe; je le fais tous les jours. Je dois respecté la DO178B (celle d'aujourd'hui, en 1970, elle n'existait pas).
Dans ce que tu décris, je ne vois rien de différent avec un test utilisant un "golden model", que l'on utilise en ce moment.
Si tu as une autre méthode moins chiante, je suis preneur.
"La première sécurité est la liberté"
[^] # Re: Se passer des tests ...
Posté par Nicolas Boulay (site web personnel) . En réponse au journal La preuve de programme : où en est-on ?. Évalué à 2.
Ben non. Cela ne marche pas que comme ça.
Si c'est pas prouvé, il te donne un contre exemple immédiatement, donc tu corriges très rapidement ton appli pas besoin de la suite de non régression "overnight". C'est sans doute la partie la plus utile.
Si c'est prouvé bingo. Si l'assertion est correctement exprimé. C'est en fait moins utile que le cas précédent.
Si il n'y arrive pas, le prouveur d'Esterel te donne une profondeur temporel genre 10 coups d'horloges, si on connait la structure de son code (pas de mémoire à plus de 10 coups en arrière), on peut être confiant.
Dans la vérification formel, j'inclus aussi la génération automatique de vecteurs d'entrée pour augmenter le taux de couverture. Il n'y a plus qu'à avoir des sorties de références ou des assertions à vérifier.
Le static timing analyser de temps en pire cas permet de te trouver ton pire cas en timing. (il faut par contre un beau modèle de ton systèm)
J'ai dû oublier d'autres types de vérification.
"La première sécurité est la liberté"
[^] # Re: ça pue c'est pas libre
Posté par Nicolas Boulay (site web personnel) . En réponse au journal La société Always Innovating porte bien son nom!. Évalué à 2.
C'est pas gagné avec un cortex A8, celui-ci dispose d'une fpu et d'instructions SIMD. Je ne suis pas sur qu'il soit moins efficace que le dsp.
Les PowerVR font un carton en ce moment dans l'embarqué
vivement opengraphics :)
"La première sécurité est la liberté"
[^] # Re: Domotique
Posté par Nicolas Boulay (site web personnel) . En réponse au journal La société Always Innovating porte bien son nom!. Évalué à 3.
J'ai toujours voulu un moyen simple (un téléphone portable ?) pour tracer les prix d'un produit entre différent magasin.
"La première sécurité est la liberté"
[^] # Re: Se passer des tests ...
Posté par Nicolas Boulay (site web personnel) . En réponse au journal La preuve de programme : où en est-on ?. Évalué à 2.
Et bossant pour une boite qui vend un "langage formel" pour ce genre d'application, je peux te dire que tout ce qui est vérification formel est loin d'être la règle, et est encore moins reconnu (sauf peut-être dans le ferroviaire et encore).
"La spécialités de mes formateurs en test de logiciels" et ils forment à quel genre de technique ?
"La première sécurité est la liberté"
[^] # Re: Se passer des tests ...
Posté par Nicolas Boulay (site web personnel) . En réponse au journal La preuve de programme : où en est-on ?. Évalué à 1.
"La première sécurité est la liberté"
[^] # Re: Se passer des tests ...
Posté par Nicolas Boulay (site web personnel) . En réponse au journal La preuve de programme : où en est-on ?. Évalué à 2.
Et toi sur quelle planète ?
J'ai l'impression qu'il y une différence entre les pratiques habituelles pour le développement live critical et ce que tu crois l'être... vu depuis un labo.
"La première sécurité est la liberté"
[^] # Re: Se passer des tests ...
Posté par Nicolas Boulay (site web personnel) . En réponse au journal La preuve de programme : où en est-on ?. Évalué à 2.
Si tu joues le jeu de la vérification formelle, tu démonteras juste que ce n'est pas prouvable. T'es bien avancé.
Renseignes toi mieux. Ce genre d'outil existe déjà et fonctionne.
par exemple : http://www.absint.com/ait/
"La première sécurité est la liberté"
[^] # Re: Se passer des tests ...
Posté par Nicolas Boulay (site web personnel) . En réponse au journal La preuve de programme : où en est-on ?. Évalué à 1.
Dans la preuve formel, tu ajoutes une assertion qui correspond à un point de spécification. La vérification formel balaye toutes les possibilités d'entrée à la recherche d'un contre exemple.
Dans le cas du test, tu es limité par les vecteurs d'entrée que tu trouves à la main alors qu'avec un moteur de preuve, tu as l'exhaustivité.
"La première sécurité est la liberté"
[^] # Re: Se passer des tests ...
Posté par Nicolas Boulay (site web personnel) . En réponse au journal La preuve de programme : où en est-on ?. Évalué à 2.
Quelle différence entre une vérification formelle et un test, ici ?
C'est pas parcque tu as réussi à formaliser les specs que les specs sont valides.
C'est évident ça. mais dans ce cas, on parle de valider la spec par celle au dessus. Au moins on peut trouver les incohérences.
Et là si tu fais pas des tests d'ergonomie...
Cela veut dire que tu codes en suivant une spec mais que tu tests en suivant autre choses ? Je te souhaite bien du courage pour expliquer d'où vient le problème à ton client ! (sa spec et pas ton code)
'est con mais c'est comme ca dans la vraie vie, souvent tu te buttes face à un client qui ne veut pas répondre (pas le temps ou ne sais pas trancher) et tu dois faire des choix.
Je commençais à comprendre que ton client ne faisait pas des avions :)
"La première sécurité est la liberté"
[^] # Re: ARM fanless...
Posté par Nicolas Boulay (site web personnel) . En réponse au journal La société Always Innovating porte bien son nom!. Évalué à 2.
"La première sécurité est la liberté"
[^] # Re: ARM fanless...
Posté par Nicolas Boulay (site web personnel) . En réponse au journal La société Always Innovating porte bien son nom!. Évalué à 6.
Le SoC inclue bien plus de chose que l'atom seul.
"La première sécurité est la liberté"
[^] # Re: ça pue c'est pas libre
Posté par Nicolas Boulay (site web personnel) . En réponse au journal La société Always Innovating porte bien son nom!. Évalué à 2.
Peut-être que la 3D du snapdragon de qualcomm est plus ouverte. La pversion la plus puissante a une puce avec l'équivalent de 2 cortex A8 à 1.5ghz avec une puissance de calcul en SIMD double (Qualcomm a fait sa propre version de l'architecture ARMV7).
http://www.hardmicro-fr.net/news-article.storyid-3422.htm
A priori, le core 3D est en provenance d'ati, donc avec potentiellement un driver libre.
http://www.netbooktech.com/tag/snapdragon-qsd8672/
"La première sécurité est la liberté"
[^] # Re: Trop beau pour être vrai
Posté par Nicolas Boulay (site web personnel) . En réponse au journal La société Always Innovating porte bien son nom!. Évalué à 3.
La qualité du clavier va rendre le produit intéressant ou pas, j'aurais aimer un écran 10" en 720p mais si le clavier fait mal au doigts c'est encore pire.
"La première sécurité est la liberté"
[^] # Re: Trop beau pour être vrai
Posté par Nicolas Boulay (site web personnel) . En réponse au journal La société Always Innovating porte bien son nom!. Évalué à 4.
"La première sécurité est la liberté"
[^] # Re: ARM fanless...
Posté par Nicolas Boulay (site web personnel) . En réponse au journal La société Always Innovating porte bien son nom!. Évalué à 6.
Le cortex A8 a un double pipeline avec exécution dans l'ordre comme le Pentium I. Cela donne une idée des perfs max.
"La première sécurité est la liberté"
[^] # Re: Trop beau pour être vrai
Posté par Nicolas Boulay (site web personnel) . En réponse au journal La société Always Innovating porte bien son nom!. Évalué à 3.
Donc pour regarder un film pas de souci mais pour naviguer sur internet, j'espère que Fennec est bien optimisé.
"La première sécurité est la liberté"
[^] # Re: Au fait
Posté par Nicolas Boulay (site web personnel) . En réponse au journal [HS] Mort au scrutin proportionnel !. Évalué à 2.
"La première sécurité est la liberté"
[^] # Re: Se passer des tests ...
Posté par Nicolas Boulay (site web personnel) . En réponse au journal La preuve de programme : où en est-on ?. Évalué à 1.
"La première sécurité est la liberté"
[^] # Re: Se passer des tests ...
Posté par Nicolas Boulay (site web personnel) . En réponse au journal La preuve de programme : où en est-on ?. Évalué à 2.
Tu as perdu quoi ? Dire que tu compares une méthode formelle (style celle de absint qui utilise un modèle cpu+mémoire) avec la simple mesure de quelques vecteur d'entrés !
Personne n'a dit que les tests offraient de garanties.
Pourquoi tu sous entends que la solution formelle serait moins bonne alors ?
Un valideur formelle ne valide pas les specs, d'où l'intérêt de mon exemple qui n'a strictement rien de fallacieux, et qui au contraire me paraît très réaliste.
Bien sur qu'elle valide les specs ! En rédigeant la spec formelle tu identifies immédiatement tous les manques et précision à demander à ton client !
"La première sécurité est la liberté"
[^] # Re: Se passer des tests ...
Posté par Nicolas Boulay (site web personnel) . En réponse au journal La preuve de programme : où en est-on ?. Évalué à 2.
"La première sécurité est la liberté"
[^] # Re: prouveur automatique/assistant de preuve
Posté par Nicolas Boulay (site web personnel) . En réponse au journal La preuve de programme : où en est-on ?. Évalué à 1.
Il n'y a pas à tortiller, si la "spec" est "le programme termine sur l'entrée 16 en temps 64", c'est trivial, si c'est "le programme calcule factorielle", c'est indécidable. Les specs que tu veux vérifier, c'est parce qu'elles sont non triviales,
Non, c'est aussi parce que le programme est gros.
Tu veux vérifier que tu ne t'es pas planté dans la copie d'une équation, dans la recopie d'une constante, que tu n'as pas de cas ou tu core dump.
"le programme calcule factorielle"
Sauf que ta spec ne dira pas ça. Il dira factoriel selon l'algo bidule précis à 10^-14 en code double flottant. De toute façon, je vois mal factoriel comme étant une fonction de base de ton logiciel de preuve.
La "preuve" sera l'équivalence à x^-14 prêt entre l'équation mathématique de la spec et ton code (souvent des développements limité).
Mais pour le cas de factoriel, le test tel que définit par la DO-178B demande de couvrir les classes d'équivalences, ce qui va se réduire à tester un nombre négatif, zéro, un nombre positif, voir les nombres max et min du range spécifié, et le range+1 pour voir que cela ne plante pas. 7 tests en tout pour vérifier l'équivalence à 10^-14 prêt et pour avoir la certif de ton avion.
Si tu fais quelques milliers de test en random() en plus, c'est encore mieux (mais la certif s'en fout). Les partitions par classe d'équivalence fonctionnent en test boite blanche quand tu connais la tête du code et que tu voix bien qu'il n'y a pas de branchement. De toute façon, à l'exécution du test, tu vérifies la couverture de code.
Certe tu n'auras pas prouver l'équivalence entre spec et code mais tu auras une grande confiance, ce qui est le principale.
"La première sécurité est la liberté"
[^] # Re: mouais
Posté par Nicolas Boulay (site web personnel) . En réponse au journal La preuve de programme : où en est-on ?. Évalué à 2.
"La première sécurité est la liberté"
[^] # Re: Se passer des tests ...
Posté par Nicolas Boulay (site web personnel) . En réponse au journal La preuve de programme : où en est-on ?. Évalué à 2.
Je ne pense pas que l'on est besoin que toutes assertions soit prouvable, j'ai peur que cela sois compliqué. Je préfère que des assertions simples (division par zéro) puisse être traité sur le programme en entier. Générer un contre exemple, c'est indispensable tellement, c'est utile.
La génération automatique de pattern de teste pour passer les assertion en dynamique pour faire la couverture de code est très utile (pour avoir le pire cas en timing aussi). Les stratégies de tests pour trouver les vecteurs sont parfaitement automatisable (gestion des classes d'équivalence, branches, valeur singulière, etc..)
"La première sécurité est la liberté"