1、1,Assertion based Verification: the Instrumentation Approach,Doron Drusinsky ,2,Background,Step 1. Specification and Validation For example: work done with Steve Raque on GRAIL,R1: once LOI burn sequence is uploaded, the orbiter will, within the time prescribed in the command sequence parameters (pl
2、us/minus t1), perform a burn for the duration prescribed in the command sequence parameters (plus/minus t2).,NL “Concern” about SUT behavior:,3,Background,Step 1 (cont.),Assertion:,public void testMe() int nTime= 0;BurnSequence seq = new BurnSequence(1000, 100);assertion.burnSequenceUploaded(seq);nT
3、ime = 1009;CDH.setTime(nTime);assertion.openedFuelValve();nTime += 96;CDH.setTime(nTime);assertion.closeFuelValve();nTime += 100;CDH.setTime(nTime);assertTrue(assertion.isSuccess(); ,Stand-alone validation testing:,4,Background,Step 1 (cont.),Create Domain Model (DM) for executable-SRM:,public void
4、testMe() .,Via-DM validation testing:,Assertion Repos,DM,5,?,Background,Step 2: Verification,SUT C/C+ Common platform for Scientific missions is VxWorks,Assertion Repository,.,6,Background,Step 2: Verification we are using Runtime Verification (RV/EMC),Drusinsky, D. Michael, J. B., and Shing, M.-T.
5、, A Visual Tradeoff Space for Formal Verification and Validation Techniques, IEEE Systems Journal, Vol. 2, No. 4, Dec 2008, pp. 513-519. ISSN: 1932-8184,7,Background,SUT C/C+ Common platform for Scientific missions is VxWorks,Execute in Special Verification VM/Environment,E.g. JPF/SPIN,Limitations:
6、1. Cannot support real-time SUT 2. Doesnt support “non-regular” specifications,SUT C/C+ Common platform for Scientific missions is VxWorks,Instrumentation,Limitations: 1. Interferes with execution,Step 2: There are two ways to perform RV:,8,Background,Step 2: Verification using instrumentation,SUT C
7、/C+ Common platform for Scientific missions is VxWorks,Assertion Repository,.,Log-file,“Execute” log-files,9,Background,Step 2: Verification (cont.),SUT C/C+ Common platform for Scientific missions is VxWorks,Assertion Repository,.,Todays presentation,10,Background,Step 2: Verification (cont.),SUT C
8、/C+ Common platform for Scientific missions is VxWorks,Assertion Repository,.,Log-Stream (sockets),“Execute” log-stream,11,Architecture,Black = existing Green = short term development Red = longer term development,12,General Idea,VxWorks - Workbench,13,General Idea,VxWorks - Workbench,Instrument src
9、,14,General Idea,VxWorks - Workbench,Build App,15,General Idea,VxWorks - Workbench,Execute on target,Execute in existing environment,16,General Idea,VxWorks - Workbench,17,General Idea,VxWorks - Workbench,18,Source Code Instrumentation Plugin,Planned Properties: End-user ease of use - Eclipse extend
10、ed GUI plugin. Work with virtually any GCC compiler. Be an Eclipse plugin. Visibility. Flexibility. Stability/Robustness Support VxWorks. Integration with StateRover Assertion Repositories.,19,Source Code Instrumentation Vs. Other Techniques,20,Basic Instrumentation GUI,Notes: C/C+ file doesnt have
11、to be compiled/built in Eclipse Will work with practically any C/C+ file that is legal for a (any) GCC compiler,21,Instrumentation Support Files,Not for public release,22,XML Log Output,XML Log file or Socket Stream:,.,Contains sequences of method calls and related timing) = test-suite,23,Extended I
12、nstrumentation GUI (1),Not for public release,24,Extended Instrumentation GUI (2),Not for public release,25,Extended Instrumentation GUI (3),Not for public release,26,Extended Instrumentation GUI (4),Not for public release,27,Extended Instrumentation GUI (5),Not for public release,28,From Log Files
13、To JUnit,VxWorks - Workbench,Reminder:,29,From Log Files To JUnit (cont.),.,Import to a Java project with the AssertionRepository (see sequel slides),Import the .log file to a Java Project and convert to JUnit (and legal XML):,30,From Log Files To JUnit (cont.),.,Select the log file from step 3 here
14、. Note! The importer can import illegal XML log files too,JUnit equivalent of .log file is generated:,31,From Log Files To JUnit (cont.),Step 6. Run the generated JUnit test against Assertion Repository,32,From Log Files To JUnit (cont.) - timing,When assertions are used for verification the timer i
15、s associated with time delays on the SUT. Always write assertions thinking in terms of milliseconds.,Currently C/C+ instrumentation has a second level of granularity the Log to JUnit import tool automatically converts those to 1000 milliseconds.If you write your own time grabber, change the unit to
16、millis if necessary,33,Some Challenges,Namespaces,SUT void openValve() . ,.,Log-file,“Execute” log-files,Assertion Repository:,openedFuelValve/,34,Some Challenges,Namespaces,SUT,.,Log-file,“Execute” log-files,Assertion Repository:,openedFuelValve/,openValve() . ,?,35,Experiments (on QNX RTOS),Target: x86 target, dual core, 2.6 MHz Speed impact: 4-5 sec per instrumented point (instrumented method) In comparison - QNXs own instrumentation tool has a hit of 12 sec per instrumented method Size: Approximately 140 bytes per instrumentation point,36,Thank you,
