Model-Based Testing (MBT) is a promising technology to extend test coverage beyond manually crafted tests, by automatically creating more, longer, and more diverse test cases, with less effort, from abstract models of the required behavior. When the models used for MBT are correct, the test cases are provably valid as well. TNO-ESI and ASML have …continue reading

It is shown how to verify requirements on the PLC code in use at Tata Steel. A translator from PLC programs to the input language for SMT solvers has been written. Subsequently, requirements on some of the largest PLC programs available at Tata steel have been written down, and their validity on the software has …continue reading