Formal Demonstrations Session

Developers are often faced with a natural language change request (such as a bug report) and tasked with identifying all code elements that must be modified in order to fulfill the request (e.g., fix a bug or implement a new feature). In order to accomplish this task, developers frequently and routinely perform change impact analysis. This formal demonstration paper presents ImpactMiner, a tool that implements an integrated approach to software change impact analysis. The proposed approach estimates an impact set using an adaptive combination of static textual analysis, dynamic execution tracing, and mining software repositories techniques. ImpactMiner is available from our online appendix http://www.cs.wm.edu/semeru/ImpactMiner/

In the era of mobile computing, developers often need to migrate code written for one platform in a programming language to another language for a different platform, e.g., from Java for Android to C# for Windows Phone. The migration process is often performed manually or semi-automatically, in which developers are required to manually define translation rules and API mappings. This paper presents semSMT, an automatic tool to migrate code written in Java to C#. semSMT utilizes statistical machine translation to automatically infer translation rules from existing migrated code, thus, requires no manual defining of rules. The video demonstration on semSMT can be found on YouTube at http://www.youtube.com/watch?v=aRSnl5-7vNo.

Software systems are often constructed by combining new and existing services and components. Models of such systems should therefore be compositional in order to reflect the architectural structure. We present herein an extension of the LTSA model checker. It supports the specification, visualisation and failure analysis of composable, probabilistic behaviour of component-based systems, modelled as Probabilistic Component Automata (PCA). To evaluate aspects such as the probability of system failure, a DTMC model can be automatically constructed from the composition of the PCA representations of each component and analysed in tools such as PRISM. Before composition, we reduce each PCA to its interface behaviour in order to mitigate state explosion associated with composite representations. Moreover, existing behavioural analysis techniques in LTSA can be applied to PCA representations to verify the compatibility of interface behaviour between components with matching provided-required interfaces. A video highlighting the main features of the tool can be found at:http://youtu.be/moIkx8JHE7o.

Issue trackers monitor the progress of software development "issues", such as bug fixes and discussions about features. Typically, developers subscribe to issues they are interested in through the tracker, and are informed of changes and new developments via automated email. In practice, however, this approach does not scale well, as developers may receive large volumes of messages that they must sort through using their mail client; over time, it becomes increasingly challenging for them to maintain awareness of the issues that are relevant to their activities and tasks. To address this problem, we present a tool called called DASH that is implemented in the form of personalized views of issues; developers indicate issues of interest and DASH presents customized views of their progress and informs them of changes as they occur. Video: http://youtu.be/Jka_MsZet20

Effectiveness of software development process depends on the accuracy of data in supporting tools. In particular, a customer issue assigned to a wrong product team takes much longer to resolve (negatively affecting user-perceived quality) and wastes developer effort. In Open Source Software (OSS) and in commercial projects values in issue-tracking systems (ITS) or Customer Relationship Management (CRM) systems are often assigned by non-developers for whom the assignment task is difficult. We propose PAR (Product Assignment Recommender) to estimate the odds that a value in the ITS is incorrect. PAR learns from the past activities in ITS and performs prediction using a logistic regression model. Our demonstrations show how PAR helps developers to focus on fixing real problems, and how it can be used to improve data accuracy in ITS by crowd-sourcing non-developers to verify and correct low-accuracy data. http://youtu.be/IuykbzSTj8s

The complexity of web application construction is increasing at an astounding rate. Developing for the web typically crosses multiple application tiers in a variety of languages, which can result in disjoint code bases. This lack of standardization introduces new challenges for reasoning. In this paper we introduce Verily, a new web framework for Java that supports the development of verifiable web applications. Rather than requiring that programs be verified in separate a posteriori analysis, Verily supports construction via a series of Recipes, which are properties of an application that are enforced at compile time. In addition to introducing the Verily framework, we also present two Recipes: the Core Recipe, an application architecture for web applications designed to replace traditional server-side Model View Controller, and the Global Mutable State Recipe, which enables developers to use sessions within their applications without resorting to the use of unrestricted global mutable state. Demo Video: http://www.youtube.com/watch?v=TjRF7E4um3c

Web service composition is an emerging technique to develop Web applications by composing existing Web services. Web service composition is subject to two important classes of requirements, i.e., functional and non-functional requirements. Both are crucial to Web service composition. Therefore, it is desirable to verify combined functional and non-functional requirements for Web service composition. We present VeriWS, a tool to verify combined functional and non-functional requirements of Web service composition. VeriWS captures the semantics of Web service composition and verifies it directly based on the semantics. We also show how to describe Web service composition and properties using VeriWS. The YouTube video for demonstration of VeriWS is available at https://sites.google.com/site/veriwstool/