Study Synoptic++ test generation with simple authentication program

[GoogleCodeExporter]

As a proof of concept, we use Synoptic++ to derive concrete tests for a simple 
authentication program. The program prompts user to enter pin. If the pin is 
correct, it grants access to the user and terminates. Otherwise, it denies 
access and prompts the user to enter pin again. The program allows user to 
enter pin at most 3 times. If at the third time the pin is incorrect, the 
program denies access to the user and terminates.

This simple authentication program has a property that we can use to 
demonstrate the usefulness of Synoptic++ in test generation. That is, the 
choice of input determines the control flow in the program. With this example, 
we want to show that choosing input value in test generation is difficult, and 
that having state invariants makes such task easier.

Original issue reported on code.google.com by rsukk...@cs.washington.edu on 25 Apr 2013 at 7:36

[GoogleCodeExporter]

Original comment by ssukkerd on 25 Apr 2013 at 7:38

• Changed state: Accepted
• Added labels: StatefulSyn

[GoogleCodeExporter]

Original comment by ssukkerd on 1 Jul 2013 at 1:26

• Changed state: Fixed