Difference Between Manual Testing and Concolic/Symbolic Testing in Software Development
Manual testing involves checking concrete input and output values for specific execution scenarios, while concolic/symbolic testing requires imagining all possible scenarios and modeling a general environment. General invariants on input and output values are described, similar to state model checking.
- Software Development
- Testing Techniques
- Manual vs Symbolic Testing
- Concolic Testing
- State Model Checking
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
E N D
Presentation Transcript
Key Difference between Manual Testing and Concolic/Symbolic Testing Manual testing A user should test one concrete execution scenario by checking a pair of concrete input values and the expected concrete output values Concolic/symbolic testing A user should imagine all possible execution scenarios and model a general environment that can enable all possible executions A user should describe general invariants on input values and output values Very similar to state model checking (see the following example) 1/11
Ex1'. Circular Queue of Positive Integers #include<stdio.h> #define SIZE 12 #define EMPTY 0 Step 1) 0 1 2 3 4 5 6 7 8 9 10 11 0 0 0 0 0 0 15 6 9 8 4 0 // We assume that q[] is // empty if head==tail unsigned int q[SIZE],head,tail; head=6 tail=11 Step 2) 3 5 0 0 0 0 15 6 9 8 4 17 void enqueue(unsigned int x) { q[tail]=x; tail=(++tail)%SIZE; } head=6 tail=2 Step 3) 3 5 0 0 0 0 0 6 9 8 4 17 unsigned int dequeue() { unsigned int ret; ret = q[head]; q[head]=0; head= (++head)%SIZE; return ret;} head=7 tail=2 2/11
void dequeue_verify() { unsigned int ret, old_head, old_tail; unsigned int old_q[SIZE], i; void enqueue_verify() { unsigned int x, old_head, old_tail; SYM_unsigned_int(x) unsigned int old_q[SIZE], i; SYM_assume(x>0);//if(!(x>0)) exit(); for(i=0; i < SIZE; i++) old_q[i]=q[i]; old_head=head; old_tail=tail; SYM_assume(head!=tail); if(!(x>0)) exit(); for(i=0; i < SIZE; i++) old_q[i]=q[i]; old_head=head; old_tail=tail; ret= ret=dequeue dequeue(); (); enqueue enqueue(x); (x); assert(ret==old_q[old_head]); assert(q[old_head]== EMPTY); assert(head==(old_head+1)%SIZE); assert(tail==old_tail); for(i=0; i < old_head; i++) assert(old_q[i]==q[i]); for(i=old_head+1; i < SIZE; i++) assert(old_q[i]==q[i]);} assert(q[old_tail]==x); assert(tail== ((old_tail +1) % SIZE)); assert(head==old_head); for(i=0; i < old_tail; i++) assert(old_q[i]==q[i]); for(i=old_tail+1; i < SIZE; i++) assert(old_q[i]==q[i]);} #include<crown.h> int main() { environment_setup(); dequeue_test();} #include<crown.h> int main() { environment_setup(); enqueue_test();}
// Initial random queue setting following the script void environment_setup() { int i; for(i=0;i<SIZE;i++) { q[i]=EMPTY;} #include<stdio.h> #define SIZE 12 #define EMPTY 0 SYM_unsigned_int(head); SYM_assume(0<= head && head < SIZE); SYM_unsigned_int(tail); SYM_assume(0<= tail && tail < SIZE); unsigned int q[SIZE],head,tail; if( head < tail) for(i=head; i < tail; i++) { SYM_unsigned_int(q[i]);SYM_assume(0< q[i]);} else if(head > tail) { for(i=0; i < tail; i++) { SYM_unsigned_int(q[i]); SYM_assume(0< q[i]);} for(i=head; i < SIZE; i++) { SYM_unsigned_int(q[i]); SYM_assume(0< q[i]);} } // We assume that q[] is empty if head==tail void enqueue(unsigned int x) { q[tail]=x; tail=(++tail)%SIZE; } unsigned int dequeue() { unsigned int ret; ret = q[head]; q[head]=0; head= (++head)%SIZE; return ret; } printf("head:%u, tail:%u\n",head, tail); if( head < tail) for(i=head; i < tail; i++) printf("q[%u]:%u\n",i,q[i]); else if(head > tail) { for(i=0; i < tail; i++) printf("q[%u]:%u\n",i,q[i]); for(i=head; i < SIZE; i++) printf("q[%u]:%u\n",i,q[i]); } }
