I have completed an exercise that demonstrates how to model stuck-faults in Alloy4 for a very simple digital circuit and to generate test vectors that detect that kind of fault in Alloy4.
This achieves Automatic Test Pattern Generation (ATPG) for stuck-at type faultss in the digital circuit under test in Alloy4.
The Alloy model benefits you, the user, with an elegant, completely transparent usage of built-in powerful SAT solvers as well as implicit, transparent, isomorphic simplication so that you get only distinct, unique test cases.
This example represents a blending of very hi-level, abstract modeling (usually reserved for software) with traditional test pattern generation for an electronic logic circuit.
It is a demonstration of how test case generation in Model-Driven Testing (MDT) can be done for hardware with an explicit, discrete, abstract, hi-level fault model.
The first download below is the 8-page PDF technical article on ATPG in Alloy4.
The second download below is the Alloy4 source (.als) code for the stuck-at model itself.
* * *
The third download is a proposal for Signed, Random Programs (SignedRP), a test method for computer platforms that leverages constrained, hi-level random program generation tools from compiler testing, the Valgrind utility and standard checksum/hash-code algorithms.
SignedRP is intended as a screening tool for the manufacturing test of a population of computers all of the same model and configuration. The expected benefit of SIRP is the detection of faults which are not detectable by non-random test algorithms or lo-level randomization.
