« September 2003 | Main | November 2003 »
October 29, 2003
[Research] BrickOS
[BrickOS] The operating system we want for the mindstorm. INcludes a C/C++ interface that is doxygen documented. Now we just have to get it, install it and see if there's a simulator/emulator for it. This is the succesor for LegOS.
Is this a symbolic model checker for BrickOS? Almost, its a tool set for "modelling, schedulability analysis, synthesis of (optimal) schedules and executable code" It had a tools paper at TACAS 2002.
Here's a more conventional simulator.
Posted by jones at 07:47 PM | Comments (0)
October 28, 2003
[Paper reviews] Transformations for Model Checking Distributed Java... by Stoller and Liu
[Transformations for Model Checking Distributed Java Programs (ResearchIndex)] Three transformations to allow the verification of a mutli-process java program in a single java process. Also avoid native library calls in the process.
The problem:
there are model checkers for multi threaded single process java programs. In java, its easy to define a multi process distributed program. There are no model checkers for multi-process distributed programs. Distributed means "programs that involve communication among multiple processes". and... RMI and encryption invoke native methods and "Supporting such native methods in a model checker is extremely problematic, because there is no general way for the model checker to save and restore their state."
The solution:
1. Centralization: "merge all processes into a single process"
2. RMI removal: replace RMI with normal method invocations.
3. Pseudo-crypto: replace cyptographic stuff with symbolic counterparts.
The limitations:
All three transformations rely on the assumption that the original program is not real-time and does not use reflection in a way that would detect the transformation's effects.
The details:
to be added later.
The results:
implementation is "mostly complete" Will be released as part of Bandera. First case study will be a scalable distributed voting system done as a class project. Should be done by SPIN 2001.
Relation to our work:
Assuming we make a model checker for C on a real time platform, there are some lessons to learn from this paper. First, as we expect, calls to native libraries are going to be difficult to model. We plan to not follow library calls into system code. This is similar to what gdb does if you "execute a funtion without descending into the function" I still think that's a fine idea.
Second, we are aiming for real time settings. Stoller and Liu deliberatly avoid real time. We may too in the end!
Posted by jones at 08:15 AM | Comments (0)
[Paper reviews] "Model checking Java programs using ..." by Groce,Visser
[Mike Jones' Mostly CS Blog: Directed Model checking for Java] resurrected from the archive.
Posted by jones at 08:06 AM | Comments (0)
October 27, 2003
[Research] C/C++ on Lego RCX
[rcx-egcs-c -1.1.2-1.i386 RPM, Web-legOS 0.1 Les Smithson C++] It may be more interesting to work in C/C++ than Java since that's where we want to go long term with our verification tool. Model checkers for Java already exist. Identifying and solving problems with a C/C++ model checker that does not use translation to another language is our next topic.
Posted by jones at 10:03 AM | Comments (0)
October 24, 2003
[Paper reviews] Guided model checking... by Edelkamp
[Mike Jones' Mostly CS Blog: Guided Model checking in HSF Spin]
Posted by jones at 06:55 PM | Comments (0)
October 22, 2003
[Paper reviews] "Logic Verification of ANSI-C..." by Holzmann
[Logic Verification of ANSI C code with SPIN by Holzmann Mercer review]
An interesting approach to verifying C code using an abstraction in SPIN.
What is the problem being addressed?
reliable verification for software systems is a tough and elusive goal--especially for distributed software. Old-school things like code reviews, lab testing and peer reviews work better for sequential and deterministic things than they do for distributed systems. Logic verification of software in general is hard because most of the interesting verification problems are undecidable. Most automated efforts to do logic verification focus on carefully constructed and syntactically defined subsets. Programmers "shun" such efforts.
What approach is being taken to solve the problem?
Extract an abstract model of a piece of C code drop the abstract model into SPIN. The default abstraction should be "sufficient to make the verification problem tractable." For "reasonable constraints (e.g., given a memory arena of 64 MB and a runtime constraint of upto 10 minutes)" the probability of missing an error should be small.
more to come...
Posted by jones at 08:53 AM | Comments (0)
October 21, 2003
[Research] Lego RCX refercnes
[an RCX simulator, RCX architecture, how to take an RCX apart, and what you'll find inside, lots of mindstorm links
Posted by jones at 09:52 AM | Comments (0)
October 20, 2003
[] iTunes on Windows XP
[PCWorld.com - Microsoft Exec Rips ITunes, iTunes for Windows: How to Copy Music Between Authorized Computers] Dave Fester is entitled to his own opinion about what Windows users want in an online music service. But for this XP user, existence is a good property. iTunes works great on my XP boxen and will work even better on my new mac laptop this February. Yes, a Family Home Eveving spent with a twin on each lapdownloading Mom and Dad's favorite songs from high school was a good time for the whole family. Surprisingly, our girls seemed to realy get into Cher's "believe."
However, it would be cool if I could... login to another computer using my iTunes account, then download my songs onto the second computer directly from the iTunes server rather than using either a USB keychain or a windows local network. iTunes can manage all the permissions on their server, it just costs more bandwidth. But that's probably the issue. Part of my 99 cents includes the bandwidth I used to get my song. But still.
Posted by jones at 07:24 PM | Comments (0)
October 16, 2003
[Misc.] Magnetic interior storm windows
[Energy-Efficient Interior Storm Windows] We are going to score a second window to put inside the window casing to cut down on draft and road noise. We'll see if it works and report back. There's not much reliable information out there on interior storm windows to reduce traffice noise. The guy at home depot said he'd try the "install a second piece of glass (or lexan or whatever) inside the window frame and see what happens first" before spending the money on hard-core storm windows.
Update 3/21/2006: I got a call this morning from the Environmental Improvement Agency. This is a copmany in Sandy that install magnetic interior storm windows. Their number is 801 571-5717. That reminded me that I haven't yet updated this entry. We built a lexan interior storm window using a poplar wood window frame. We got a good sound reduction out of that, but it was ugly and clunky. So we used our tax return and installed double paned vinyl windows with an extra layer of laminate throughout the house. That made a noticeable difference in our road noise.
Magnetic interior storm windows would probably have given us about the same amount of reduction (because the dead air space is larger) for less money but we couldn't find a good local supplier. However, The EIA called this morning and they've been doing it in Utah for 15 years! Hopefully putting their info here will get them connected with the next person trying to solve this problem in their house.
Posted by jones at 01:13 PM
[Misc.] My famous friend Brandt Demars
[Crews near completion of Deer Creek Dam upgrade :: The Daily Herald , ESPN bottom 10 comments] Brandt got 1 quote in ESPN and 1 quote in the Daily Herald so far this week. I don't think either of us have had a quote anywhere for years now. At least since Brandt's now famous use of orange juice to make cement on a bridge signage project in southern Utah that was reported in the Daily Universe.
Posted by jones at 09:06 AM | Comments (0)
October 13, 2003
[Paper reviews] Bytecode Model Checking: An Experimental Analysis
[Bytecode Model Checking: An Experimental Analysis - Basin, Friedrich, Gawkowski, Posegga (ResearchIndex)] Construct an abstract model of all byte code instructions that modifies the JVM state recorded in the type signature used in Java byte code verification. State the type safety properties as invariants. Check if the sequence of type manipulations represented by the program are type safe. Works pretty good. Explicit better than symbolic. Best suited for applications that need high confidence and don't have time or memory constraints during verification (such as off line verification of java for use on smart cards).
1. Main problem:
When a user downloads a java program, the JVM performs a static analysis of the byte code to ensure that the byte code meets certain requirements required to securely execute the byte code on the host JVM. This is usually done by a polynomial dataflow analysis algorithm. The paper explores potentially exponential model checking algorithms for doing the same thing. The problem with the dataflow algorithm is that it marks certain kinds of valid programs as invalid (such as classes that use "subroutines in different contexts"). Using a model checker to do the bytecode verification results in a precise characterization of valid and invalid programs but requries more time and space. This is useful in settings where precise correctness is important, but time and space resources are not. In some settings, such a JVMs for smart cards, the bytecode verification is done off-line and signed. This is an application in which model checking for bytecode verification makes sense.
2. Approach to solving the problem.
For each Java bytecode instruction, define an abstract operation that modifies the JVM state visible to the type system. The type system keeps track of the program counter, the stack and the registers. Each instruction is translated into its effect on the current type. Thus instruction execution is simply traversal through a set of types. This solves problems with multiple inheritance (for each type, take its maximal supertype and call that the current type. That's hard if a type has several different super types) and multiple return values. The verification works by checking that certain type safety conditions, like the stack doesn't overflow, hold at every program point. In SPIN, this is done by checking "always type-safe". Here's some sample promela code they've generated:
proctype transitions( ) {
do
:: pc==0 -> atomic { opst[opst_ptr]=loc[1]; opst_ptr=opst_ptr+1; pc=1 };
:: pc==2 -> atomic { opst[opst_ptr]=13; opst_ptr=opst_ptr+1; pc=3 };
:: pc==3 -> atomic { break };
3. What is the authors claim about their approach?
Claim #1 Model checking for byte code verification is slower but more accurate than static analysis. Claim #2 Explicit state ennumeation is more efficient for this problem than symbolic methods.4. How do the authors support their claim?
By verifying the byte code for all the methods in the java.lang package.Posted by jones at 09:17 AM | Comments (0)
[Research] SPIN 2001, 2002 Proceedings
[SPIN 2001, LNCS volume 2051 , SPIN 2002, LNCS volume 2318] An interesting conference on explicit model checking. Papers we/I need to read are...
From 2002 proceedings
Bytecode Model Checking: An Experimental Analysis by Basin, Friedrich et al
Partial Order Reduction in Directed Model Checking by Lluch-Lafuenta, Edelkamp and LeueFrom 2001 proceedings
Transformations for Model Checking Distributed Java Programs by Stoller and LiuPosted by jones at 08:31 AM | Comments (0)
October 09, 2003
[Research] Java for Lego Mindstorms
[leJOS] Mindstorms have concurrency, and this is a java interface. This may be a reasonable platform for toy projects in verification of thread interactions in embedded devices?
Posted by jones at 02:51 PM | Comments (0)
[Tech Support] Java Swing Componets and how to use them
[A Visual Index to the Swing Components, a simple example]
Posted by jones at 01:14 PM | Comments (0)
[Paper reviews] "Formal Analysis of the Remote.." by Havelund
[Formal Analysis of the Remote Agent Before and After Flight - Havelund, Lowry, Park, Pecheur, Penix, Visser, White (ResearchIndex)] This is a methodology paper about using explicit model checkers to find concurrency errors in space flight software written in Java. This is a rare methodology paper in the sense that the authors were able to analyze a non-intentional bug that occured during deployment in a working piece of code.
1. What problem is being addressed?
NASA wants to launch a remote agent into space. They'd like some reassurance, before the launch, that the RA will function correctly. This is a hard problem because a flight control system is built on several microprocessors using complex concurrent software. Complex concurrent software is difficult to debug. Explicit state model checking is a good tool for debugging complex concurrent software, but explicit model checkers suffer from capacity limits and input language limits. The real problem is that NASA wants/needs to be convinced that explicit model checking can result in more reliable flight control systems.2. What approach is being taken to solve the problem?
The authors completed two case studies in which they applied EMC to the RA. In the first, they translated a hunk of LISP code to PROMELA and ran spin on an abstraction of the resulting PROMELA. This required alot of work and was an inspiration for the java pathfinder. Using SPIN located 5 high-quality we-couldn't-have-found-them errors. When the mission was in flight, the controller experienced a deadlock. The second verification effort was a case study to find the deadlock that occured in space. The deadlock was found and was isomorphic to one of the original 5 errors.
In the second case study, the verification team got a copy of all the java code and nothing else. They set up a front end "review team" to look over the code and identify regions likelty to contain the error. They set up a back end team to recieve the code identified by the front end team and actually find the error. The review team identified about 700 lines of code. they turned that 700 lines of code over to the JPF the JPF translated it into promela and spin found the error.
More specifically, the error depended on a missing critical section around a conditional wait.3. What is the claim about the approach?
"formal methods tools can find concurrency errors that indeed lead to loss of spacecraft functions, even for complex software required for autonomy"4. How do the authors support their claim?
The claim is an existence claim. They support their claim by showing that such an error has been found using SPIN.5. Do you believe they established their claim?
Yes.6. How does their approach, claim and justification relate to your problem and solution?
The deadlock that happened in flight was caused by a race condition between two concurrent threads. We are argueing that threads are the main problem in flight controll software.Posted by jones at 10:58 AM | Comments (0)
October 08, 2003
[Tech Support] Numbered Pseudocode in Latex
Numbererd pseudocode has line numbers that proceede each line of your pseudocode, as you might have guessed. The latex is...
\begin{figure}
% --------------------------------------------------
\noindent
\newcounter{alines}
\begin{list}{\arabic{alines}\ \ }{\usecounter{alines}}
\item \textbf{Algorithm Conciousness}
\item while (1)
\labe{line:example}
\item \ \ \ wait to recieve message;
\item \ \ \ if message = startDFS1 then DFS1
\item \ \ \ if message = (startDFS2, trace) then DFS2 (trace)
\item \ \ \ if message = abort then kill DFS1 and/or DFS2
\item endwhile
\item ...
\end{list}
\caption{Parts of the BEE algorithm.}
\label{fig:searches}
\end{figure}As an added bonus, if you add \label entries on the line just below an \item, the label will refer to that particular line number. So in this example, \ref{line:example} refers to the line number of the line containing "while(1)"
Posted by jones at 09:42 AM | Comments (0)
October 07, 2003
[Tech Support] Doxygen, and how to use it
[Doxygen] is a free tool for generating HTML docuemtnation from existing C/C++, Java and other kinds of programs. It works pretty good, if you get some of the key options right. The most useful and obscure optoins for my purposes are...
Works great.
- EXTRACT_ALL = YES to extract all functions, not just the commented ones.
- HAVE_DOT=YES to use dot to generate inheritance and call graphs.
- CALL_GRAPH=YES to generate call graphs for glabal functions.
- RECURSIVE=YES to recurse into source subdirectories,
- FILE_PATTERNS= = *.h *.c *.C *.inc *.cpp to get all my .C source files.
Posted by jones at 10:32 PM | Comments (0)
[Misc.] Moab hiking trails
[Moab Area Hiking Trails, Negro Bill Canyon, BLM trails] Planning for the annual Thanksgiving trip to Moab. We'll take the twins up Mill Creek trail and I'll go for my day-after-thanksgiving trail run up Negro Bill Canyon.
Posted by jones at 07:19 AM | Comments (0)
October 04, 2003
[Misc.] Logarithm Identities
[Properties of Logarithms] I can never remember these.
Posted by jones at 11:54 AM | Comments (0)
[Tech Support] My next stats book
[Amazon.com: Books: Probability and Statistics (3rd Edition)]
Posted by jones at 09:10 AM | Comments (0)
October 03, 2003
[Research] NSF CFPs
[Highly Dependable Computing and Communication Systems Research nsf03557] Reads like dependability research to me. But this one on embedded systems might be more relevant.
Posted by jones at 08:43 AM | Comments (0)
October 02, 2003
[Tech Support] Auto C++ to HTML documentation
[Documentation Tools] Robodoc appears to require a great deal of extra annotation. Not real useful for a large existing code base like ours. Doc++ had a bad checksum in the rpm. my fault? oh well. Doxygen seemsto work pretty good. Be sure to set EXTRACT_ALL=YES in the config file. Can we extract even unstructured comments intelligently? Maybe the GUI will be easier to use. Well, maybe not. Its missing a shared library it needs. We'll stick to the text with documentation.
Posted by jones at 10:00 PM | Comments (0)
[Tech Support] More about getting ppoint or excel into eps and tex
[Getting Postscript figures into and out of Windows applications, LaTeX2e tricks, miktex] so that's all good except I get text blanked out because the bounding box is too big. try \epsfig{figure=foo.epsi,clip=}
Posted by jones at 09:03 PM | Comments (0)
[Research] SC travel plans
Conference dates: Nov 15-21 (Monday tutorials, Tuesday it starts, Friday is panels). I will plan to leave Sunday night for Phoenix. The morning tutorial on mpi2 looks interesting as does the afternoon tutorial on Performance analysis looks interesting. and leave Thursday night.
technical program starts on 11/18 goes through 11/20.
Depart Sunday 16th around 830 for PHX depart Thursday around 940 for SLC.
T20919.Posted by jones at 06:28 PM | Comments (0)
[Research] LNCS Class from Springer
[Springer-Verlag - LNCS] where to get the latex class files for formating a paper in LNCS style.
Posted by jones at 10:34 AM | Comments (0)
[Tech Support] paragraph columns in latex tables
The LaTeX Tabular Environment \begin{tabular}{|l|l|p{2.5in}|} makes a column that's 2.5in wide and splits lines to fit the width.
Posted by jones at 08:49 AM | Comments (0)
October 01, 2003
[Research] Considerations for Airborn Systems and Equipment
Posted by jones at 06:29 AM | Comments (1)