EECS4315

User Tools

Site Tools

You are here: Mission Critical Systems » Lab 8
Trace:
lab8

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Next revision		Previous revision
Next revisionBoth sides next revision
lab8 [2016/03/02 19:30] – created francklab8 [2017/03/02 15:00] – franck
Line 1: Line 1:
-Implement a listener and publisher that, given the following app,+====== Lab 8 ====== 
 + 
 + 
 +Consider the following app.
 <html> <html>
 <pre> <pre>
-import java.util.Random; +public class ComputeSquareRoot {
- +
-public class Example {+
     public static void main(String[] args) {     public static void main(String[] args) {
- Random random = new Random(); +          double data = 3.1415926; 
- if (random.nextBoolean()) { +          System.out.println("The square root of " + data + " is " + StrictMath.sqrt(data));
-     System.out.println("true"); +
- } else { +
-     System.out.println("false"); +
- }+
     }     }
 } }
 </pre> </pre>
 </html> </html>
-and the application configuration file 
-<html> 
-<pre> 
-target=Example 
-classpath=. 
-native_classpath=. 
-listener=AmountOfNonDeterminism 
  
-</pre> +  - Develop a model class so that the above app can be verified with JPF.  [[https://en.wikipedia.org/wiki/Methods_of_computing_square_roots|This]] Wikipedia page might be helpful. 
-</html> +  - Develop a native peer so that the above app can be verified with JPF.
-produces output similar to +
-<html> +
-<pre> +
-JavaPathfinder core system v8.0 (rev 29) - (C) 2005-2014 United States Government. All rights reserved. +
- +
- +
-====================================================== system under test +
-Example.main() +
- +
-====================================================== search started: 3/2/16 2:27 PM +
-false +
-true +
- +
-====================================================== +
-maximum amount of nondeterminism: 2 choice(s) +
- +
-====================================================== results +
-no errors detected +
- +
-====================================================== statistics +
-elapsed time:       00:00:00 +
-states:             new=1,visited=0,backtracked=1,end=1 +
-search:             maxDepth=1,constraints=0 +
-choice generators:  thread=1 (signal=0,lock=1,sharedRef=0,threadApi=0,reschedule=0), data=0 +
-heap:               new=352,released=12,maxLive=0,gcCycles=1 +
-instructions:       3176 +
-max memory:         56MB +
-loaded code:        classes=61,methods=1332 +
- +
-====================================================== search finished: 3/2/16 2:27 PM +
-</pre> +
-</html> +
-Apart from the classes that have been discussed in the lectures, also the class ChoiceGenerator, which is part of the package gov.nasa.jpf.vm, may be useful.+
  
lab8.txt · Last modified: 2017/03/03 15:55 by franck