Formalization Of Digital Circuits Using The B Method
Author(s)
J-L Boulanger, A Aljer & G Mariano
Abstract
The goal of this paper is to show how it is possible to combine the advantages of the B method in order to design secure (secure in this paper means more than correct, the design performe what the client wants, furthermore it garantees to note achieve the unwanted cases) digital circuits that may be easily developed and does not need a design test. The circuit design may be based on the libraries of well-known circuit design language like VHDL. Our goal is to make use of B method to produce the electronic or numeric circuits. At the beginning, the circuit specifications are written in the abstract machine. The refinement direction is determined by the basic elements which are used to constuct the desired circuit. So the designer can orient the development to the needed level. This level can be found as a basic library in B. We demonstrate how VHDL packages can be tanslated as B circuit components for giving to the designer a high-level view. Using this approach, one can develop a circuit of which each part of which all the specification parts has already been proven to be correct.
Keywords
Related Book
Other papers in this volume
Warning (2)
: foreach() argument must be of type array|object, null given [in
/var/www/dce7ae55-385b-4ffa-8595-3ec5e61ff110/public_html/app/templates/Papers/view.php, line
364]
Code
$counter = '0';
foreach ($paper['book']['Paper'] as $otherPaper) {
if ((!empty($otherPaper['name'])) && ($counter < '7') && ($otherPaper['available'] == 1)) {
Cake\Error\ErrorTrap->handleError() /var/www/dce7ae55-385b-4ffa-8595-3ec5e61ff110/public_html/app/templates/Papers/view.php, line 364
/var/www/dce7ae55-385b-4ffa-8595-3ec5e61ff110/public_html/app/vendor/cakephp/cakephp/src/View/View.php /var/www/dce7ae55-385b-4ffa-8595-3ec5e61ff110/public_html/app/vendor/cakephp/cakephp/src/View/View.php, line 1188
Cake\View\View->_evaluate() /var/www/dce7ae55-385b-4ffa-8595-3ec5e61ff110/public_html/app/vendor/cakephp/cakephp/src/View/View.php, line 1145
Cake\View\View->_render() /var/www/dce7ae55-385b-4ffa-8595-3ec5e61ff110/public_html/app/vendor/cakephp/cakephp/src/View/View.php, line 785
Cake\View\View->render() /var/www/dce7ae55-385b-4ffa-8595-3ec5e61ff110/public_html/app/vendor/cakephp/cakephp/src/Controller/Controller.php, line 712
Cake\Controller\Controller->render() /var/www/dce7ae55-385b-4ffa-8595-3ec5e61ff110/public_html/app/vendor/cakephp/cakephp/src/Controller/Controller.php, line 516
Cake\Controller\Controller->invokeAction() /var/www/dce7ae55-385b-4ffa-8595-3ec5e61ff110/public_html/app/vendor/cakephp/cakephp/src/Controller/ControllerFactory.php, line 166
Cake\Controller\ControllerFactory->handle() /var/www/dce7ae55-385b-4ffa-8595-3ec5e61ff110/public_html/app/vendor/cakephp/cakephp/src/Controller/ControllerFactory.php, line 141
Cake\Controller\ControllerFactory->invoke() /var/www/dce7ae55-385b-4ffa-8595-3ec5e61ff110/public_html/app/vendor/cakephp/cakephp/src/Http/BaseApplication.php, line 362
Cake\Http\BaseApplication->handle() /var/www/dce7ae55-385b-4ffa-8595-3ec5e61ff110/public_html/app/vendor/cakephp/cakephp/src/Http/Runner.php, line 86
Cake\Http\Runner->handle() /var/www/dce7ae55-385b-4ffa-8595-3ec5e61ff110/public_html/app/vendor/cakephp/cakephp/src/Http/Middleware/CsrfProtectionMiddleware.php, line 169
Cake\Http\Middleware\CsrfProtectionMiddleware->process() /var/www/dce7ae55-385b-4ffa-8595-3ec5e61ff110/public_html/app/vendor/cakephp/cakephp/src/Http/Runner.php, line 82
Cake\Http\Runner->handle() /var/www/dce7ae55-385b-4ffa-8595-3ec5e61ff110/public_html/app/vendor/cakephp/cakephp/src/Http/Middleware/BodyParserMiddleware.php, line 157
Cake\Http\Middleware\BodyParserMiddleware->process() /var/www/dce7ae55-385b-4ffa-8595-3ec5e61ff110/public_html/app/vendor/cakephp/cakephp/src/Http/Runner.php, line 82
Cake\Http\Runner->handle() /var/www/dce7ae55-385b-4ffa-8595-3ec5e61ff110/public_html/app/vendor/cakephp/cakephp/src/Routing/Middleware/RoutingMiddleware.php, line 118
Cake\Routing\Middleware\RoutingMiddleware->process() /var/www/dce7ae55-385b-4ffa-8595-3ec5e61ff110/public_html/app/vendor/cakephp/cakephp/src/Http/Runner.php, line 82
Cake\Http\Runner->handle() /var/www/dce7ae55-385b-4ffa-8595-3ec5e61ff110/public_html/app/vendor/cakephp/cakephp/src/Routing/Middleware/AssetMiddleware.php, line 69
Cake\Routing\Middleware\AssetMiddleware->process() /var/www/dce7ae55-385b-4ffa-8595-3ec5e61ff110/public_html/app/vendor/cakephp/cakephp/src/Http/Runner.php, line 82
Cake\Http\Runner->handle() /var/www/dce7ae55-385b-4ffa-8595-3ec5e61ff110/public_html/app/vendor/cakephp/cakephp/src/Error/Middleware/ErrorHandlerMiddleware.php, line 115
Cake\Error\Middleware\ErrorHandlerMiddleware->process() /var/www/dce7ae55-385b-4ffa-8595-3ec5e61ff110/public_html/app/vendor/cakephp/cakephp/src/Http/Runner.php, line 82
Cake\Http\Runner->handle() /var/www/dce7ae55-385b-4ffa-8595-3ec5e61ff110/public_html/app/vendor/cakephp/debug_kit/src/Middleware/DebugKitMiddleware.php, line 60
DebugKit\Middleware\DebugKitMiddleware->process() /var/www/dce7ae55-385b-4ffa-8595-3ec5e61ff110/public_html/app/vendor/cakephp/cakephp/src/Http/Runner.php, line 82
Cake\Http\Runner->handle() /var/www/dce7ae55-385b-4ffa-8595-3ec5e61ff110/public_html/app/vendor/cakephp/cakephp/src/Http/Runner.php, line 60
Cake\Http\Runner->run() /var/www/dce7ae55-385b-4ffa-8595-3ec5e61ff110/public_html/app/vendor/cakephp/cakephp/src/Http/Server.php, line 104
Cake\Http\Server->run() /var/www/dce7ae55-385b-4ffa-8595-3ec5e61ff110/public_html/app/webroot/index.php, line 37
[main]
