LOGIN TO YOUR ACCOUNT

Username
Password
Remember Me
Or use your Academic/Social account:

CREATE AN ACCOUNT

Or use your Academic/Social account:

Congratulations!

You have just completed your registration at OpenAire.

Before you can login to the site, you will need to activate your account. An e-mail will be sent to you with the proper instructions.

Important!

Please note that this site is currently undergoing Beta testing.
Any new content you create is not guaranteed to be present to the final version of the site upon release.

Thank you for your patience,
OpenAire Dev Team.

Close This Message

CREATE AN ACCOUNT

Name:
Username:
Password:
Verify Password:
E-mail:
Verify E-mail:
*All Fields Are Required.
Please Verify You Are Human:
fbtwitterlinkedinvimeoflicker grey 14rssslideshare1
Kimmitt, Jonathan R. R. (2015)
Languages: English
Types: Doctoral thesis
Subjects:
The increasing commoditization of computers in modern society has exceeded the\ud pace of associated developments in reliability. Although theoretical computer science\ud has advanced greatly in the last thirty years, many of the best techniques have yet to\ud find their way into embedded computers, and their failure can have a great potential\ud for disrupting society.\ud This dissertation presents some approaches to improve computer reliability using\ud software and hardware techniques, and makes the following claims for novelty: innovative\ud development of a toolchain and libraries to support extraction from dependent type\ud checking in a theorem prover; conceptual design and deployment in reconfigurable\ud hardware; an extension of static type-safety to hardware description language and\ud FPGA level; elimination of legacy C code from the target and toolchain; a novel\ud hardware error detection scheme is described and compared with conventional triple\ud modular redundancy. The elimination of any user control of memory management\ud promotes robustness against buffer overruns, and consequently prevents vulnerability\ud to common Trojan techniques.\ud The methodology identifies type punning as a key weakness of commonly encountered\ud embedded languages such as C, in particular the extreme difficulty of determining if\ud an array access is in bounds, or if dynamic memory has been properly allocated and\ud released. A method of eliminating dependence on type-unsafe libraries is presented, in\ud conjunction with code that has optionally been proved correct according to user-defined\ud criteria. An appropriately defined subset of OCaml is chosen with support for the Coq\ud theorem prover in mind, and then evaluated with a custom backend that supports\ud behavioural Verilog, as well as a fixed execution unit and associated control store.\ud Results are presented for this alternative platform for reliable embedded systems\ud development that may be used in future industrial flows.\ud To provide assurance of correct operation, the proven software needs to be executed in\ud an environment where errors are checked and corrected in conjunction with appropriate\ud exception processing in the event of an uncorrectable error. Therefore, the present\ud author’s previously published error detection scheme based on dual-rail logic and\ud self-checking checkers is further developed and compared with traditional N-modular\ud redundancy
  • No references.
  • No related research data.
  • No similar publications.

Share - Bookmark

Cite this article