Interview: How does a Model Checker work?

Model Checking is part of the Formal Methods which address formal specification, formal development, formal verification and theorem provers. Model Checking belongs to the formal verification and provides a complete mathematical proof to verify your system-under-test. BTC EmbeddedPlatform uses the model checking technology for structural test data generation to achieve full code coverage, for formal […]

When and how to generate test cases automatically

The automatic test case generation has always been a controversial topic. While some people dream about stopping any manual test activities others say that test generation is not allowed. But who is right? Test Goals for automatic test case generation Let’s have a quick look at the possible test goals for which we can generate […]

The Power of Focus – How to Optimize a Model Checker for Embedded Software

1. Focus on effectiveness to solve the problem of your customer! Since day one we address exactly the problem classes our customer needs to solve, i.e. large-sized auto-generated embedded code –on the one hand– with integer, floating point and pointer arithmetic, large look-up tables, and state-flow logic but –on the other hand– even without recursive functions, memory allocation, and […]