Formal specification with B (Q2757791)

Le livre ``Spécification formelle avec B'' est une introduction à la notation B et à la méthode B. La méthode B a été elaborée par J.-R. Abrial pour spécifier, concevoir et coder des systèmes logiciels. Le concept de base est celui de machine abstraite dont l'état est décrit par un invariant. La méthode consiste à prouver formellement que les opérations respectent bien l'invariant, puis à raffiner les machines abstraites en machines implantables, et à prouver que ce raffinage est correct.NEWLINENEWLINENEWLINELa méthode B est utilisée dans l'industrie, notamment dans les systèmes de sécurité, de protection et de contrôle de vitesse des trains.