Lab 7

Formal verification and testing

You will find below two demos of the BTC Embedded Platform for formal verification and test generation. Due to the current epidemiological situation we find yourselves forced to replace the actual hands-on specification and verification (which are only possible live), with this demo-based introduction. The BTC Embedded Platform is a powerful tool used for the verification and automated testing of embedded systems. It offers a formal specification framework to intuitively express and analyze requirements of automotive systems, a formal verification tool making use of several well known model-checkers, and a tool for automated test generation and formal testing, where one can both generate tests from requirements, measure how the tests cover the specified requirements etc.

Formal specification and verification

First, go through the steps described in the specification tutorial available here. You won't be able to actually try them remotely, but it's important to understand how the requirements are gradually transformed from informal to semi-formal and, finally, to a formal specification.

Then watch the demo up to about 11:00. Pause it, and then go through the verification tutorial provided here. Pay attention to how a proof is configured (search depth, loop unroll, the available model-checking core engines etc.), all these are aspects around which optimizations have been performed in order to keep the verification process as fast and scalable as possible. Note that, in case of an error being found, the resulting counter-example trace can be then used to debug the available model, and can also be converted to a test. Watch the rest of the demo, which presents the actual verification: creating and running the proof for specified requirements.

https://vimeo.com/479597598/91a8354dfb

Formal test generation

Similarly, before watching the video, go through the formal testing and automated test generation tutorial here. Pay attention specifically to the relation between tests and requirements, and how the test coverage of requirements is being considered. Take a look at the available types of reports that can be generated based on the test suite in the profile. Then, go ahead and watch the demo.

https://vimeo.com/479600105/ffe2698bee