[CSUSB]>> [CNS]>> [CSE]>> [R J Botting]>> biba.php
Bibliographic Item (1.0)
- Yonit Kesten & Amit Klein & Amir Pnueli & Gil Raanan
- Bridging the E-Business Gap Through Formal Verification
- =EXPERIENCE VERIFICATION DESIGN SECURITY MODULE SAFETY SPIN SPL SPL++ PROMELA STeP C++
- How to formulate a C++ class in SPL++.
- Proves a composition rule for safety channel properties.
- Safety properties: once failed they are never again met.
- Top-level design took nearly 7 hours to verify using SPIN/Linux on 333MHz Pentium-II.
- Used manual verification for the detailed C++. Calls for deductive verification tools that can handle threaded C++.
Search for bibliographic items containing a matching string.
Search for a specific bibliographic item by name.
To see the complete bibliography (1Mb+) select:[Bibliography]