Mining Scenarios with Value-Based Invariants

Supporting Materials

David Lo (Singapore Management University) and Shahar Maoz (RWTH-Aachen University, Germany)

Abstract

Specification mining takes execution traces as input and extracts likely program invariants, which can be used for comprehension, verification, and evolution related tasks. In this work we integrate scenario-based specification mining, which uses data-mining algorithms to suggest ordering constraints in the form of live sequence charts, an inter-object, visual, modal, scenario-based specification language, with mining of value-based invariants, which detects likely invariants holding at specific program points. On top of the mining algorithms, we distinguish the scenario-specific invariants from the regular ones using a technique we call scenario-based slicing. The resulting suggested specifications are rich, consisting of modal scenarios annotated with scenario-specific value-based invariants, referring to event parameters and participating object properties.

An evaluation of our work over a number of case studies shows promising results in extracting expressive specifications from real programs, which could not be extracted previously. The more expressive the mined specifications, the higher their potential to support program comprehension and testing.

Case Study

Machine Settings:
              Intel Core2 Duo 2.40GHz 3.24GB RAM Windows XP Tablet PC
              Mining program is written using C#.Net 2.0 compiled using VS.Net 2005

Target Applications:

              CrossFTP - a commercial open source FTP server
              Jeti - a popular instant messaging application

Symbol mappings in paper to actual class names:

CrossFTP
CTM - org.apache.ftpserver.gui.FtpConnectionTableModel
BU - org.apache.ftpserver.usermanager.BaseUser
ENV - environment
FRI - org.apache.ftpserver.FtpRequestImpl
PASV - org.apache.ftpserver.command.PASV
DC - org.apache.ftpserver.FtpDataConnection
DCC - org.apache.ftpserver.DataConnectionConfig
SSL - org.apache.ftpserver.ssl.Ssl
FW - org.apache.ftpserver.FtpWriter
STOR - org.apache.ftpserver.command.STOR
PWD - org.apache.ftpserver.command.PWD
STAT - org.apache.ftpserver.command.STAT
CL - org.apache.ftpserver.commandline.CommandLine
SF - org.apache.ftpserver.gui.ServerFrame

Jeti
JH - nu.fw.jeti.backend.JabberHandler
Jabber - nu.fw.jeti.backend.Jabber
CWS - nu.fw.jeti.ui.ChatWindows
CW - nu.fw.jeti.ui.ChatWindow
PC - nu.fw.jeti.plugins.drawing.shapes.PictureChat
PC$1 - nu.fw.jeti.plugins.drawing.shapes.PictureChat$1
PH - nu.fw.jeti.plugins.drawing.shapes.PictureHistory
C - nu.fw.jeti.plugins.drawing.shapes.actions.Creation
HP - nu.fw.jeti.plugins.drawing.ui.HistoryPanel

Experimental Datasets and Results: exp-dataset-result.zip

Extended Case Study