SA-17(04) - Correspondance informelle (PbMM)
Énoncés :
Exiger que la développeuse ou le développeur du système, du composant du système ou du service qui s’y rapporte s’assure de :
a. produire, en parfaite intégration avec le processus de développement, des spécifications descriptives informelles de haut niveau qui décrivent les interfaces du matériel, des logiciels et des micrologiciels servant à la sécurité sur le plan des exceptions, des messages d’erreur et des effets
b. montrer par [Sélection (un choix) : démonstration informelle; arguments convaincants fournis, si possible, par des méthodes formelles] que les spécifications descriptives de haut niveau sont conformes au modèle formel de stratégie
c. montrer, par des démonstrations informelles, que les spécifications descriptives de haut niveau prennent en compte toutes les interfaces du matériel, des logiciels et des micrologiciels servant à la sécurité
d. montrer que les spécifications descriptives de haut niveau décrivent précisément les interfaces du matériel, des logiciels et des micrologiciels servant à la sécurité
e. décrire les mécanismes liés au matériel, aux logiciels et aux micrologiciels servant à la sécurité qui ne sont pas explicitement pris en compte dans les spécifications descriptives de haut niveau, mais qui sont strictement inhérents à ce matériel, à ces logiciels et à ces micrologiciels servant à la sécurité
La correspondance est un élément important de l’assurance gagnée en cours de modélisation. Elle démontre que la mise en œuvre constitue une transformation précise du modèle, et que le code ou le détail de mise en œuvre additionnel n’aura aucune incidence sur les comportements ou les stratégies en cours de modélisation. La cohérence entre les spécifications descriptives de haut niveau (par exemple, une conception de haut niveau ou de bas niveau) et le modèle formel de stratégie est généralement impossible à prouver hors de tout doute. Par conséquent, une combinaison de méthodes formelles et informelles pourrait être requise pour démontrer la cohérence. Les mécanismes liés au matériel, aux logiciels et aux micrologiciels, qui sont strictement inhérents au matériel, aux logiciels et aux micrologiciels servant à la sécurité, comprennent les registres de mappage, ainsi que les entrées et sorties directes liées à la mémoire.