FSE 2014 – Author Index |
Contents -
Abstracts -
Authors
Online Calendar - iCal File |
A B C D F G H J K L M N P R S T W X Y Z
Alves, Everton L. G. |
FSE '14-DEMO: "RefDistiller: A Refactoring ..."
RefDistiller: A Refactoring Aware Code Review Tool for Inspecting Manual Refactoring Edits
Everton L. G. Alves, Myoungkyu Song, and Miryung Kim (University of Texas at Austin, USA; Federal University of Campina Grande, Brazil; University of California at Los Angeles, USA) Manual refactoring edits are error prone, as refactoring requires developers to coordinate related transformations and understand the complex inter-relationship between affected types, methods, and variables. We present RefDistiller, a refactoring-aware code review tool that can help developers detect potential behavioral changes in manual refactoring edits. It first detects the types and locations of refactoring edits by comparing two program versions. Based on the reconstructed refactoring information, it then detects potential anomalies in refactoring edits using two techniques: (1) a template-based checker for detecting missing edits and (2) a refactoring separator for detecting extra edits that may change a program's behavior. By helping developers be aware of deviations from pure refactoring edits, RefDistiller can help developers have high confidence about the correctness of manual refactoring edits. RefDistiller is available as an Eclipse plug-in at https://sites.google.com/site/refdistiller/ and its demonstration video is available at http://youtu.be/0Iseoc5HRpU. @InProceedings{FSE14p751, author = {Everton L. G. Alves and Myoungkyu Song and Miryung Kim}, title = {RefDistiller: A Refactoring Aware Code Review Tool for Inspecting Manual Refactoring Edits}, booktitle = {Proc.\ FSE}, publisher = {ACM}, pages = {751--754}, doi = {}, year = {2014}, } |
|
Autili, Marco |
FSE '14-DEMO: "CHOReOSynt: Enforcing Choreography ..."
CHOReOSynt: Enforcing Choreography Realizability in the Future Internet
Marco Autili, Davide Di Ruscio, Amleto Di Salle, and Alexander Perucci (University of L'Aquila, Italy) Choreographies are an emergent Service Engineering (SE) approach to compose together and coordinate services in a distributed way. A choreography formalizes the way business participants coordinate their interactions. The focus is not on orchestrations of the work performed within them, but rather on the exchange of messages between these participants. The problems usually addressed when considering a choreography-based specification of the system to be realized are realizability check, and conformance check. In this paper we describe the CHOReOSynt tool, which has been conceived to deal with an additional problem, namely, automated choreography enforcement. That is, when the goal is to actually realize a service choreography by reusing third-party services, their uncontrolled (or wrongly coordinated) composite behavior may show undesired interactions that preclude the choreography realization. CHOReOSynt solves this problem by automatically synthesizing additional software entities that, when interposed among the services, allow for preventing undesired interactions. Screencast: http://choreos.disim.univaq.it/downloads/ @InProceedings{FSE14p723, author = {Marco Autili and Davide Di Ruscio and Amleto Di Salle and Alexander Perucci}, title = {CHOReOSynt: Enforcing Choreography Realizability in the Future Internet}, booktitle = {Proc.\ FSE}, publisher = {ACM}, pages = {723--726}, doi = {}, year = {2014}, } |
|
Baltes, Sebastian |
FSE '14-DEMO: "Linking Sketches and Diagrams ..."
Linking Sketches and Diagrams to Source Code Artifacts
Sebastian Baltes, Peter Schmitz, and Stephan Diehl (University of Trier, Germany) Recent studies have shown that sketches and diagrams play an important role in the daily work of software developers. If these visual artifacts are archived, they are often detached from the source code they document, because there is no ad- equate tool support to assist developers in capturing, archiving, and retrieving sketches related to certain source code artifacts. This paper presents SketchLink, a tool that aims at increasing the value of sketches and diagrams created during software development by supporting developers in these tasks. Our prototype implementation provides a web application that employs the camera of smartphones and tablets to capture analog sketches, but can also be used on desktop computers to upload, for instance, computer-generated diagrams. We also implemented a plugin for a Java IDE that embeds the links in Javadoc comments and visualizes them in situ in the source code editor as graphical icons. @InProceedings{FSE14p743, author = {Sebastian Baltes and Peter Schmitz and Stephan Diehl}, title = {Linking Sketches and Diagrams to Source Code Artifacts}, booktitle = {Proc.\ FSE}, publisher = {ACM}, pages = {743--746}, doi = {}, year = {2014}, } |
|
Becker, Steffen |
FSE '14-DEMO: "A Tool Suite for the Model-Driven ..."
A Tool Suite for the Model-Driven Software Engineering of Cyber-Physical Systems
Stefan Dziwok, Christopher Gerking, Steffen Becker, Sebastian Thiele, Christian Heinzemann, and Uwe Pohlmann (University of Paderborn, Germany; Fraunhofer IPT, Germany) Cyber-physical systems, e.g., autonomous cars or trains, interact with their physical environment. As a consequence, they commonly have to coordinate with other systems via complex message communication while realizing safety-critical and real-time tasks. As a result, those systems should be correct by construction. Software architects can achieve this by using the MechatronicUML process and language. This paper presents the MechatronicUML Tool Suite that offers unique features to support the MechatronicUML modeling and analyses tasks. @InProceedings{FSE14p715, author = {Stefan Dziwok and Christopher Gerking and Steffen Becker and Sebastian Thiele and Christian Heinzemann and Uwe Pohlmann}, title = {A Tool Suite for the Model-Driven Software Engineering of Cyber-Physical Systems}, booktitle = {Proc.\ FSE}, publisher = {ACM}, pages = {715--718}, doi = {}, year = {2014}, } |
|
Cai, Yuanfang |
FSE '14-DEMO: "Titan: A Toolset That Connects ..."
Titan: A Toolset That Connects Software Architecture with Quality Analysis
Lu Xiao, Yuanfang Cai, and Rick Kazman (Drexel University, USA; University of Hawaii, USA) In this tool demo, we will illustrate our tool---Titan---that supports a new architecture model: design rule spaces (DRSpaces). We will show how Titan can capture both architecture and evolutionary structure and help to bridge the gap between architecture and defect prediction. We will demo how to use our toolset to capture hundreds of buggy files into just a few architecturally related groups, and to reveal architecture issues that contribute to the error-proneness and change-proneness of these groups. Our tool has been used to analyze dozens of large-scale industrial projects, and has demonstrated its ability to provide valuable direction on which parts of the architecture are problematic, and on why, when, and how to refactor. The video demo of Titan can be found at https://art.cs.drexel.edu/~lx52/titan.mp4 @InProceedings{FSE14p763, author = {Lu Xiao and Yuanfang Cai and Rick Kazman}, title = {Titan: A Toolset That Connects Software Architecture with Quality Analysis}, booktitle = {Proc.\ FSE}, publisher = {ACM}, pages = {763--766}, doi = {}, year = {2014}, } |
|
Cleland-Huang, Jane |
FSE '14-DEMO: "Archie: A Tool for Detecting, ..."
Archie: A Tool for Detecting, Monitoring, and Preserving Architecturally Significant Code
Mehdi Mirakhorli, Ahmed Fakhry, Artem Grechko, Matteusz Wieloch, and Jane Cleland-Huang (Rochester Institute of Technology, USA; DePaul University, USA) The quality of a software architecture is largely dependent upon the underlying architectural decisions at the framework, tactic, and pattern levels. Decisions to adopt certain solutions determine the extent to which desired qualities such as security, availability, and performance are achieved in the delivered system. In this tool demo, we present our Eclipse plug-in named Archie as a solution for maintaining architectural qualities in the design and code despite long-term maintenance and evolution activities. Archie detects architectural tactics such as heartbeat, resource pooling, and role-based access control (RBAC) in the source code of a project; constructs traceability links between the tactics, design models, rationales and source code; and then uses these to monitor the environment for architecturally significant changes and to keep developers informed of underlying design decisions and their associated rationales. @InProceedings{FSE14p739, author = {Mehdi Mirakhorli and Ahmed Fakhry and Artem Grechko and Matteusz Wieloch and Jane Cleland-Huang}, title = {Archie: A Tool for Detecting, Monitoring, and Preserving Architecturally Significant Code}, booktitle = {Proc.\ FSE}, publisher = {ACM}, pages = {739--742}, doi = {}, year = {2014}, } |
|
Diehl, Stephan |
FSE '14-DEMO: "Linking Sketches and Diagrams ..."
Linking Sketches and Diagrams to Source Code Artifacts
Sebastian Baltes, Peter Schmitz, and Stephan Diehl (University of Trier, Germany) Recent studies have shown that sketches and diagrams play an important role in the daily work of software developers. If these visual artifacts are archived, they are often detached from the source code they document, because there is no ad- equate tool support to assist developers in capturing, archiving, and retrieving sketches related to certain source code artifacts. This paper presents SketchLink, a tool that aims at increasing the value of sketches and diagrams created during software development by supporting developers in these tasks. Our prototype implementation provides a web application that employs the camera of smartphones and tablets to capture analog sketches, but can also be used on desktop computers to upload, for instance, computer-generated diagrams. We also implemented a plugin for a Java IDE that embeds the links in Javadoc comments and visualizes them in situ in the source code editor as graphical icons. @InProceedings{FSE14p743, author = {Sebastian Baltes and Peter Schmitz and Stephan Diehl}, title = {Linking Sketches and Diagrams to Source Code Artifacts}, booktitle = {Proc.\ FSE}, publisher = {ACM}, pages = {743--746}, doi = {}, year = {2014}, } |
|
Dig, Danny |
FSE '14-DEMO: "BumbleBee: A Refactoring Environment ..."
BumbleBee: A Refactoring Environment for Spreadsheet Formulas
Felienne Hermans and Danny Dig (Delft University of Technology, Netherlands; Oregon State University, USA) Spreadsheets are widely used in industry. It is estimated that end-user programmers outnumber regular programmers by a factor of 5. However, spreadsheets are error-prone: several reports exist of companies that have lost big sums of money due to spreadsheet errors. In previous work, spreadsheet smells have proven to be the cause of some of these errors. To that end, we have developed a tool that can apply refactorings to spreadsheet formulas, implementing our previous work on spreadsheet refactoring, which showed that spreadsheet formula smells are very common and that refactorings for them are widely applicable and that refactoring them with a tool is both quicker and less error-prone. Our new tool Bumblebee is able to execute refactorings originating from both these papers, by means of an extensible syntax, and can furthermore apply refactorings on entire groups of formulas, thus improving upon the existing tool RefBook. Finally, BumbleBee can also execute transformations other than refactorings. @InProceedings{FSE14p747, author = {Felienne Hermans and Danny Dig}, title = {BumbleBee: A Refactoring Environment for Spreadsheet Formulas}, booktitle = {Proc.\ FSE}, publisher = {ACM}, pages = {747--750}, doi = {}, year = {2014}, } |
|
Di Ruscio, Davide |
FSE '14-DEMO: "CHOReOSynt: Enforcing Choreography ..."
CHOReOSynt: Enforcing Choreography Realizability in the Future Internet
Marco Autili, Davide Di Ruscio, Amleto Di Salle, and Alexander Perucci (University of L'Aquila, Italy) Choreographies are an emergent Service Engineering (SE) approach to compose together and coordinate services in a distributed way. A choreography formalizes the way business participants coordinate their interactions. The focus is not on orchestrations of the work performed within them, but rather on the exchange of messages between these participants. The problems usually addressed when considering a choreography-based specification of the system to be realized are realizability check, and conformance check. In this paper we describe the CHOReOSynt tool, which has been conceived to deal with an additional problem, namely, automated choreography enforcement. That is, when the goal is to actually realize a service choreography by reusing third-party services, their uncontrolled (or wrongly coordinated) composite behavior may show undesired interactions that preclude the choreography realization. CHOReOSynt solves this problem by automatically synthesizing additional software entities that, when interposed among the services, allow for preventing undesired interactions. Screencast: http://choreos.disim.univaq.it/downloads/ @InProceedings{FSE14p723, author = {Marco Autili and Davide Di Ruscio and Amleto Di Salle and Alexander Perucci}, title = {CHOReOSynt: Enforcing Choreography Realizability in the Future Internet}, booktitle = {Proc.\ FSE}, publisher = {ACM}, pages = {723--726}, doi = {}, year = {2014}, } |
|
Di Salle, Amleto |
FSE '14-DEMO: "CHOReOSynt: Enforcing Choreography ..."
CHOReOSynt: Enforcing Choreography Realizability in the Future Internet
Marco Autili, Davide Di Ruscio, Amleto Di Salle, and Alexander Perucci (University of L'Aquila, Italy) Choreographies are an emergent Service Engineering (SE) approach to compose together and coordinate services in a distributed way. A choreography formalizes the way business participants coordinate their interactions. The focus is not on orchestrations of the work performed within them, but rather on the exchange of messages between these participants. The problems usually addressed when considering a choreography-based specification of the system to be realized are realizability check, and conformance check. In this paper we describe the CHOReOSynt tool, which has been conceived to deal with an additional problem, namely, automated choreography enforcement. That is, when the goal is to actually realize a service choreography by reusing third-party services, their uncontrolled (or wrongly coordinated) composite behavior may show undesired interactions that preclude the choreography realization. CHOReOSynt solves this problem by automatically synthesizing additional software entities that, when interposed among the services, allow for preventing undesired interactions. Screencast: http://choreos.disim.univaq.it/downloads/ @InProceedings{FSE14p723, author = {Marco Autili and Davide Di Ruscio and Amleto Di Salle and Alexander Perucci}, title = {CHOReOSynt: Enforcing Choreography Realizability in the Future Internet}, booktitle = {Proc.\ FSE}, publisher = {ACM}, pages = {723--726}, doi = {}, year = {2014}, } |
|
Dong, Jin Song |
FSE '14-DEMO: "RaPiD: A Toolkit for Reliability ..."
RaPiD: A Toolkit for Reliability Analysis of Non-deterministic Systems
Lin Gui, Jun Sun, Yang Liu , Truong Khanh Nguyen, and Jin Song Dong (National University of Singapore, Singapore; Singapore University of Technology and Design, Singapore; Nanyang Technological University, Singapore) Non-determinism in concurrent or distributed software systems (i.e., various possible execution orders among different distributed components) presents new challenges to the existing reliability analysis methods based on Markov chains. In this work, we present a toolkit RaPiD for the reliability analysis of non-deterministic systems. Taking Markov decision process as reliability model, RaPiD can help in the analysis of three fundamental and rewarding aspects regarding software reliability. First, to have reliability assurance on a system, RaPiD can synthesize the overall system reliability given the reliability values of system components. Second, given a requirement on the overall system reliability, RaPiD can distribute the reliability requirement to each component. Lastly, RaPiD can identify the component that affects the system reliability most significantly. RaPiD has been applied to analyze several real-world systems including a financial stock trading system, a proton therapy control system and an ambient assisted living room system. @InProceedings{FSE14p727, author = {Lin Gui and Jun Sun and Yang Liu and Truong Khanh Nguyen and Jin Song Dong}, title = {RaPiD: A Toolkit for Reliability Analysis of Non-deterministic Systems}, booktitle = {Proc.\ FSE}, publisher = {ACM}, pages = {727--730}, doi = {}, year = {2014}, } Video Info |
|
Dziwok, Stefan |
FSE '14-DEMO: "A Tool Suite for the Model-Driven ..."
A Tool Suite for the Model-Driven Software Engineering of Cyber-Physical Systems
Stefan Dziwok, Christopher Gerking, Steffen Becker, Sebastian Thiele, Christian Heinzemann, and Uwe Pohlmann (University of Paderborn, Germany; Fraunhofer IPT, Germany) Cyber-physical systems, e.g., autonomous cars or trains, interact with their physical environment. As a consequence, they commonly have to coordinate with other systems via complex message communication while realizing safety-critical and real-time tasks. As a result, those systems should be correct by construction. Software architects can achieve this by using the MechatronicUML process and language. This paper presents the MechatronicUML Tool Suite that offers unique features to support the MechatronicUML modeling and analyses tasks. @InProceedings{FSE14p715, author = {Stefan Dziwok and Christopher Gerking and Steffen Becker and Sebastian Thiele and Christian Heinzemann and Uwe Pohlmann}, title = {A Tool Suite for the Model-Driven Software Engineering of Cyber-Physical Systems}, booktitle = {Proc.\ FSE}, publisher = {ACM}, pages = {715--718}, doi = {}, year = {2014}, } |
|
Fakhry, Ahmed |
FSE '14-DEMO: "Archie: A Tool for Detecting, ..."
Archie: A Tool for Detecting, Monitoring, and Preserving Architecturally Significant Code
Mehdi Mirakhorli, Ahmed Fakhry, Artem Grechko, Matteusz Wieloch, and Jane Cleland-Huang (Rochester Institute of Technology, USA; DePaul University, USA) The quality of a software architecture is largely dependent upon the underlying architectural decisions at the framework, tactic, and pattern levels. Decisions to adopt certain solutions determine the extent to which desired qualities such as security, availability, and performance are achieved in the delivered system. In this tool demo, we present our Eclipse plug-in named Archie as a solution for maintaining architectural qualities in the design and code despite long-term maintenance and evolution activities. Archie detects architectural tactics such as heartbeat, resource pooling, and role-based access control (RBAC) in the source code of a project; constructs traceability links between the tactics, design models, rationales and source code; and then uses these to monitor the environment for architecturally significant changes and to keep developers informed of underlying design decisions and their associated rationales. @InProceedings{FSE14p739, author = {Mehdi Mirakhorli and Ahmed Fakhry and Artem Grechko and Matteusz Wieloch and Jane Cleland-Huang}, title = {Archie: A Tool for Detecting, Monitoring, and Preserving Architecturally Significant Code}, booktitle = {Proc.\ FSE}, publisher = {ACM}, pages = {739--742}, doi = {}, year = {2014}, } |
|
Fischer, Bernd |
FSE '14-DEMO: "ConceptCloud: A Tagcloud Browser ..."
ConceptCloud: A Tagcloud Browser for Software Archives
Gillian J. Greene and Bernd Fischer (Stellenbosch University, South Africa) ConceptCloud is an interactive browser for SVN and Git repositories. Its main novelty is the combination of an intuitive tag cloud interface with an underlying concept lattice that provides a formal structure for navigation. This combination allows users to explore repositories serendipitously, without predefined search goals and along different navigation paths. ConceptCloud can derive different lattice types for a repository and supports concurrent navigation in multiple linked tag clouds that can each be individually customized, which allows multi-faceted repository explorations. @InProceedings{FSE14p759, author = {Gillian J. Greene and Bernd Fischer}, title = {ConceptCloud: A Tagcloud Browser for Software Archives}, booktitle = {Proc.\ FSE}, publisher = {ACM}, pages = {759--762}, doi = {}, year = {2014}, } |
|
Galeotti, Juan Pablo |
FSE '14-DEMO: "XMLMate: Evolutionary XML ..."
XMLMate: Evolutionary XML Test Generation
Nikolas Havrikov, Matthias Höschele, Juan Pablo Galeotti, and Andreas Zeller (Saarland University, Germany) Generating system inputs satisfying complex constraints is still a challenge for modern test generators. We present XMLMATE, a search-based test generator specially aimed at XML-based systems. XMLMATE leverages program structure, existing XML schemas, and XML inputs to generate, mutate, recombine, and evolve valid XML inputs. Over a set of seven XML-based systems, XMLMATE detected 31 new unique failures in production code, all triggered by system inputs and thus true alarms. @InProceedings{FSE14p719, author = {Nikolas Havrikov and Matthias Höschele and Juan Pablo Galeotti and Andreas Zeller}, title = {XMLMate: Evolutionary XML Test Generation}, booktitle = {Proc.\ FSE}, publisher = {ACM}, pages = {719--722}, doi = {}, year = {2014}, } Video Info |
|
Gerking, Christopher |
FSE '14-DEMO: "A Tool Suite for the Model-Driven ..."
A Tool Suite for the Model-Driven Software Engineering of Cyber-Physical Systems
Stefan Dziwok, Christopher Gerking, Steffen Becker, Sebastian Thiele, Christian Heinzemann, and Uwe Pohlmann (University of Paderborn, Germany; Fraunhofer IPT, Germany) Cyber-physical systems, e.g., autonomous cars or trains, interact with their physical environment. As a consequence, they commonly have to coordinate with other systems via complex message communication while realizing safety-critical and real-time tasks. As a result, those systems should be correct by construction. Software architects can achieve this by using the MechatronicUML process and language. This paper presents the MechatronicUML Tool Suite that offers unique features to support the MechatronicUML modeling and analyses tasks. @InProceedings{FSE14p715, author = {Stefan Dziwok and Christopher Gerking and Steffen Becker and Sebastian Thiele and Christian Heinzemann and Uwe Pohlmann}, title = {A Tool Suite for the Model-Driven Software Engineering of Cyber-Physical Systems}, booktitle = {Proc.\ FSE}, publisher = {ACM}, pages = {715--718}, doi = {}, year = {2014}, } |
|
Grechko, Artem |
FSE '14-DEMO: "Archie: A Tool for Detecting, ..."
Archie: A Tool for Detecting, Monitoring, and Preserving Architecturally Significant Code
Mehdi Mirakhorli, Ahmed Fakhry, Artem Grechko, Matteusz Wieloch, and Jane Cleland-Huang (Rochester Institute of Technology, USA; DePaul University, USA) The quality of a software architecture is largely dependent upon the underlying architectural decisions at the framework, tactic, and pattern levels. Decisions to adopt certain solutions determine the extent to which desired qualities such as security, availability, and performance are achieved in the delivered system. In this tool demo, we present our Eclipse plug-in named Archie as a solution for maintaining architectural qualities in the design and code despite long-term maintenance and evolution activities. Archie detects architectural tactics such as heartbeat, resource pooling, and role-based access control (RBAC) in the source code of a project; constructs traceability links between the tactics, design models, rationales and source code; and then uses these to monitor the environment for architecturally significant changes and to keep developers informed of underlying design decisions and their associated rationales. @InProceedings{FSE14p739, author = {Mehdi Mirakhorli and Ahmed Fakhry and Artem Grechko and Matteusz Wieloch and Jane Cleland-Huang}, title = {Archie: A Tool for Detecting, Monitoring, and Preserving Architecturally Significant Code}, booktitle = {Proc.\ FSE}, publisher = {ACM}, pages = {739--742}, doi = {}, year = {2014}, } |
|
Greene, Gillian J. |
FSE '14-DEMO: "ConceptCloud: A Tagcloud Browser ..."
ConceptCloud: A Tagcloud Browser for Software Archives
Gillian J. Greene and Bernd Fischer (Stellenbosch University, South Africa) ConceptCloud is an interactive browser for SVN and Git repositories. Its main novelty is the combination of an intuitive tag cloud interface with an underlying concept lattice that provides a formal structure for navigation. This combination allows users to explore repositories serendipitously, without predefined search goals and along different navigation paths. ConceptCloud can derive different lattice types for a repository and supports concurrent navigation in multiple linked tag clouds that can each be individually customized, which allows multi-faceted repository explorations. @InProceedings{FSE14p759, author = {Gillian J. Greene and Bernd Fischer}, title = {ConceptCloud: A Tagcloud Browser for Software Archives}, booktitle = {Proc.\ FSE}, publisher = {ACM}, pages = {759--762}, doi = {}, year = {2014}, } |
|
Gu, Ming |
FSE '14-DEMO: "Tsmart-GalsBlock: A Toolkit ..."
Tsmart-GalsBlock: A Toolkit for Modeling, Validation, and Synthesis of Multi-clocked Embedded Systems
Yu Jiang , Hehua Zhang, Huafeng Zhang, Xinyan Zhao, Han Liu, Chengnian Sun, Xiaoyu Song, Ming Gu, and Jiaguang Sun (Tsinghua University, China; University of California at Davis, USA) The key challenges of the model-driven approach to designing multi-clocked embedded systems are three-fold: (1) how to model local synchronous components and asynchronous communication between components in a single framework, (2) how to ensure the correctness of the model, and (3) how to maintain the consistency between the model and the implementation of the system. In this paper, we present Tsmart, a self-contained toolkit to address these three challenges. Tsmart seamlessly integrates (1) a graphical editor to facilitate the modeling of the complex behaviors and structures in an embedded system, (2) a simulator for interactive graphical simulation to understand and debug the system model, (3) a verication engine to verify the correctness of the system design, and (4) a synthesis engine to automatically generate ecient executable VHDL code from the model. The toolkit has been successfully applied to designing the main control system of a train communication controller, and the system has already been deployed and in operation. The evaluation of Tsmart on this real industrial application demonstrates the eectiveness and the potential of the toolkit. @InProceedings{FSE14p711, author = {Yu Jiang and Hehua Zhang and Huafeng Zhang and Xinyan Zhao and Han Liu and Chengnian Sun and Xiaoyu Song and Ming Gu and Jiaguang Sun}, title = {Tsmart-GalsBlock: A Toolkit for Modeling, Validation, and Synthesis of Multi-clocked Embedded Systems}, booktitle = {Proc.\ FSE}, publisher = {ACM}, pages = {711--714}, doi = {}, year = {2014}, } |
|
Gui, Lin |
FSE '14-DEMO: "RaPiD: A Toolkit for Reliability ..."
RaPiD: A Toolkit for Reliability Analysis of Non-deterministic Systems
Lin Gui, Jun Sun, Yang Liu , Truong Khanh Nguyen, and Jin Song Dong (National University of Singapore, Singapore; Singapore University of Technology and Design, Singapore; Nanyang Technological University, Singapore) Non-determinism in concurrent or distributed software systems (i.e., various possible execution orders among different distributed components) presents new challenges to the existing reliability analysis methods based on Markov chains. In this work, we present a toolkit RaPiD for the reliability analysis of non-deterministic systems. Taking Markov decision process as reliability model, RaPiD can help in the analysis of three fundamental and rewarding aspects regarding software reliability. First, to have reliability assurance on a system, RaPiD can synthesize the overall system reliability given the reliability values of system components. Second, given a requirement on the overall system reliability, RaPiD can distribute the reliability requirement to each component. Lastly, RaPiD can identify the component that affects the system reliability most significantly. RaPiD has been applied to analyze several real-world systems including a financial stock trading system, a proton therapy control system and an ambient assisted living room system. @InProceedings{FSE14p727, author = {Lin Gui and Jun Sun and Yang Liu and Truong Khanh Nguyen and Jin Song Dong}, title = {RaPiD: A Toolkit for Reliability Analysis of Non-deterministic Systems}, booktitle = {Proc.\ FSE}, publisher = {ACM}, pages = {727--730}, doi = {}, year = {2014}, } Video Info |
|
Havrikov, Nikolas |
FSE '14-DEMO: "XMLMate: Evolutionary XML ..."
XMLMate: Evolutionary XML Test Generation
Nikolas Havrikov, Matthias Höschele, Juan Pablo Galeotti, and Andreas Zeller (Saarland University, Germany) Generating system inputs satisfying complex constraints is still a challenge for modern test generators. We present XMLMATE, a search-based test generator specially aimed at XML-based systems. XMLMATE leverages program structure, existing XML schemas, and XML inputs to generate, mutate, recombine, and evolve valid XML inputs. Over a set of seven XML-based systems, XMLMATE detected 31 new unique failures in production code, all triggered by system inputs and thus true alarms. @InProceedings{FSE14p719, author = {Nikolas Havrikov and Matthias Höschele and Juan Pablo Galeotti and Andreas Zeller}, title = {XMLMate: Evolutionary XML Test Generation}, booktitle = {Proc.\ FSE}, publisher = {ACM}, pages = {719--722}, doi = {}, year = {2014}, } Video Info |
|
He, Jifeng |
FSE '14-DEMO: "Aalta: An LTL Satisfiability ..."
Aalta: An LTL Satisfiability Checker over Infinite/Finite Traces
Jianwen Li , Yinbo Yao, Geguang Pu , Lijun Zhang, and Jifeng He (East China Normal University, China; Institute of Software at Chinese Academy of Sciences, China) Linear Temporal Logic (LTL) is been widely used nowadays in verification and AI. Checking satisfiability of LTL formulas is a fundamental step in removing possible errors in LTL assertions. We present in this paper Aalta, a new LTL satisfiability checker, which supports satisfiability checking for LTL over both infinite and finite traces. Aalta leverages the power of modern SAT solvers. We have conducted a comprehensive comparison between Aalta and other LTL satisfiability checkers, and the experimental results show that Aalta is very competitive. The tool is available at www.lab205.org/aalta. @InProceedings{FSE14p731, author = {Jianwen Li and Yinbo Yao and Geguang Pu and Lijun Zhang and Jifeng He}, title = {Aalta: An LTL Satisfiability Checker over Infinite/Finite Traces}, booktitle = {Proc.\ FSE}, publisher = {ACM}, pages = {731--734}, doi = {}, year = {2014}, } |
|
Heinzemann, Christian |
FSE '14-DEMO: "A Tool Suite for the Model-Driven ..."
A Tool Suite for the Model-Driven Software Engineering of Cyber-Physical Systems
Stefan Dziwok, Christopher Gerking, Steffen Becker, Sebastian Thiele, Christian Heinzemann, and Uwe Pohlmann (University of Paderborn, Germany; Fraunhofer IPT, Germany) Cyber-physical systems, e.g., autonomous cars or trains, interact with their physical environment. As a consequence, they commonly have to coordinate with other systems via complex message communication while realizing safety-critical and real-time tasks. As a result, those systems should be correct by construction. Software architects can achieve this by using the MechatronicUML process and language. This paper presents the MechatronicUML Tool Suite that offers unique features to support the MechatronicUML modeling and analyses tasks. @InProceedings{FSE14p715, author = {Stefan Dziwok and Christopher Gerking and Steffen Becker and Sebastian Thiele and Christian Heinzemann and Uwe Pohlmann}, title = {A Tool Suite for the Model-Driven Software Engineering of Cyber-Physical Systems}, booktitle = {Proc.\ FSE}, publisher = {ACM}, pages = {715--718}, doi = {}, year = {2014}, } |
|
Hermans, Felienne |
FSE '14-DEMO: "BumbleBee: A Refactoring Environment ..."
BumbleBee: A Refactoring Environment for Spreadsheet Formulas
Felienne Hermans and Danny Dig (Delft University of Technology, Netherlands; Oregon State University, USA) Spreadsheets are widely used in industry. It is estimated that end-user programmers outnumber regular programmers by a factor of 5. However, spreadsheets are error-prone: several reports exist of companies that have lost big sums of money due to spreadsheet errors. In previous work, spreadsheet smells have proven to be the cause of some of these errors. To that end, we have developed a tool that can apply refactorings to spreadsheet formulas, implementing our previous work on spreadsheet refactoring, which showed that spreadsheet formula smells are very common and that refactorings for them are widely applicable and that refactoring them with a tool is both quicker and less error-prone. Our new tool Bumblebee is able to execute refactorings originating from both these papers, by means of an extensible syntax, and can furthermore apply refactorings on entire groups of formulas, thus improving upon the existing tool RefBook. Finally, BumbleBee can also execute transformations other than refactorings. @InProceedings{FSE14p747, author = {Felienne Hermans and Danny Dig}, title = {BumbleBee: A Refactoring Environment for Spreadsheet Formulas}, booktitle = {Proc.\ FSE}, publisher = {ACM}, pages = {747--750}, doi = {}, year = {2014}, } |
|
Höschele, Matthias |
FSE '14-DEMO: "XMLMate: Evolutionary XML ..."
XMLMate: Evolutionary XML Test Generation
Nikolas Havrikov, Matthias Höschele, Juan Pablo Galeotti, and Andreas Zeller (Saarland University, Germany) Generating system inputs satisfying complex constraints is still a challenge for modern test generators. We present XMLMATE, a search-based test generator specially aimed at XML-based systems. XMLMATE leverages program structure, existing XML schemas, and XML inputs to generate, mutate, recombine, and evolve valid XML inputs. Over a set of seven XML-based systems, XMLMATE detected 31 new unique failures in production code, all triggered by system inputs and thus true alarms. @InProceedings{FSE14p719, author = {Nikolas Havrikov and Matthias Höschele and Juan Pablo Galeotti and Andreas Zeller}, title = {XMLMate: Evolutionary XML Test Generation}, booktitle = {Proc.\ FSE}, publisher = {ACM}, pages = {719--722}, doi = {}, year = {2014}, } Video Info |
|
Jiang, Yu |
FSE '14-DEMO: "Tsmart-GalsBlock: A Toolkit ..."
Tsmart-GalsBlock: A Toolkit for Modeling, Validation, and Synthesis of Multi-clocked Embedded Systems
Yu Jiang , Hehua Zhang, Huafeng Zhang, Xinyan Zhao, Han Liu, Chengnian Sun, Xiaoyu Song, Ming Gu, and Jiaguang Sun (Tsinghua University, China; University of California at Davis, USA) The key challenges of the model-driven approach to designing multi-clocked embedded systems are three-fold: (1) how to model local synchronous components and asynchronous communication between components in a single framework, (2) how to ensure the correctness of the model, and (3) how to maintain the consistency between the model and the implementation of the system. In this paper, we present Tsmart, a self-contained toolkit to address these three challenges. Tsmart seamlessly integrates (1) a graphical editor to facilitate the modeling of the complex behaviors and structures in an embedded system, (2) a simulator for interactive graphical simulation to understand and debug the system model, (3) a verication engine to verify the correctness of the system design, and (4) a synthesis engine to automatically generate ecient executable VHDL code from the model. The toolkit has been successfully applied to designing the main control system of a train communication controller, and the system has already been deployed and in operation. The evaluation of Tsmart on this real industrial application demonstrates the eectiveness and the potential of the toolkit. @InProceedings{FSE14p711, author = {Yu Jiang and Hehua Zhang and Huafeng Zhang and Xinyan Zhao and Han Liu and Chengnian Sun and Xiaoyu Song and Ming Gu and Jiaguang Sun}, title = {Tsmart-GalsBlock: A Toolkit for Modeling, Validation, and Synthesis of Multi-clocked Embedded Systems}, booktitle = {Proc.\ FSE}, publisher = {ACM}, pages = {711--714}, doi = {}, year = {2014}, } |
|
Kazman, Rick |
FSE '14-DEMO: "Titan: A Toolset That Connects ..."
Titan: A Toolset That Connects Software Architecture with Quality Analysis
Lu Xiao, Yuanfang Cai, and Rick Kazman (Drexel University, USA; University of Hawaii, USA) In this tool demo, we will illustrate our tool---Titan---that supports a new architecture model: design rule spaces (DRSpaces). We will show how Titan can capture both architecture and evolutionary structure and help to bridge the gap between architecture and defect prediction. We will demo how to use our toolset to capture hundreds of buggy files into just a few architecturally related groups, and to reveal architecture issues that contribute to the error-proneness and change-proneness of these groups. Our tool has been used to analyze dozens of large-scale industrial projects, and has demonstrated its ability to provide valuable direction on which parts of the architecture are problematic, and on why, when, and how to refactor. The video demo of Titan can be found at https://art.cs.drexel.edu/~lx52/titan.mp4 @InProceedings{FSE14p763, author = {Lu Xiao and Yuanfang Cai and Rick Kazman}, title = {Titan: A Toolset That Connects Software Architecture with Quality Analysis}, booktitle = {Proc.\ FSE}, publisher = {ACM}, pages = {763--766}, doi = {}, year = {2014}, } |
|
Kim, Miryung |
FSE '14-DEMO: "Critics: An Interactive Code ..."
Critics: An Interactive Code Review Tool for Searching and Inspecting Systematic Changes
Tianyi Zhang, Myoungkyu Song, and Miryung Kim (University of California at Los Angeles, USA; University of Texas at Austin, USA) During peer code reviews, developers often examine program differences. When using existing program differencing tools, it is difficult for developers to inspect systematic changes—similar, related changes that are scattered across multiple files. Developers cannot easily answer questions such as "what other code locations changed similar to this change?" and "are there any other locations that are similar to this code but are not updated?" In this paper, we demonstrate Critics, an Eclipse plug-in that assists developers in inspecting systematic changes. It (1) allows developers to customize a context-aware change template, (2) searches for systematic changes using the template, and (3) detects missing or inconsistent edits. Developers can interactively refine the customized change template to see corresponding search results. Critics has potential to improve developer productivity in inspecting large, scattered edits during code reviews. The tool's demonstration video is available at https://www.youtube.com/watch?v=F2D7t_Z5rhk @InProceedings{FSE14p755, author = {Tianyi Zhang and Myoungkyu Song and Miryung Kim}, title = {Critics: An Interactive Code Review Tool for Searching and Inspecting Systematic Changes}, booktitle = {Proc.\ FSE}, publisher = {ACM}, pages = {755--758}, doi = {}, year = {2014}, } Video Info FSE '14-DEMO: "RefDistiller: A Refactoring ..." RefDistiller: A Refactoring Aware Code Review Tool for Inspecting Manual Refactoring Edits Everton L. G. Alves, Myoungkyu Song, and Miryung Kim (University of Texas at Austin, USA; Federal University of Campina Grande, Brazil; University of California at Los Angeles, USA) Manual refactoring edits are error prone, as refactoring requires developers to coordinate related transformations and understand the complex inter-relationship between affected types, methods, and variables. We present RefDistiller, a refactoring-aware code review tool that can help developers detect potential behavioral changes in manual refactoring edits. It first detects the types and locations of refactoring edits by comparing two program versions. Based on the reconstructed refactoring information, it then detects potential anomalies in refactoring edits using two techniques: (1) a template-based checker for detecting missing edits and (2) a refactoring separator for detecting extra edits that may change a program's behavior. By helping developers be aware of deviations from pure refactoring edits, RefDistiller can help developers have high confidence about the correctness of manual refactoring edits. RefDistiller is available as an Eclipse plug-in at https://sites.google.com/site/refdistiller/ and its demonstration video is available at http://youtu.be/0Iseoc5HRpU. @InProceedings{FSE14p751, author = {Everton L. G. Alves and Myoungkyu Song and Miryung Kim}, title = {RefDistiller: A Refactoring Aware Code Review Tool for Inspecting Manual Refactoring Edits}, booktitle = {Proc.\ FSE}, publisher = {ACM}, pages = {751--754}, doi = {}, year = {2014}, } |
|
Kochhar, Pavneet Singh |
FSE '14-DEMO: "BugLocalizer: Integrated Tool ..."
BugLocalizer: Integrated Tool Support for Bug Localization
Ferdian Thung, Tien-Duy B. Le, Pavneet Singh Kochhar, and David Lo (Singapore Management University, Singapore) To manage bugs that appear in a software, developers often make use of a bug tracking system such as Bugzilla. Users can report bugs that they encounter in such a system. Whenever a user reports a new bug report, developers need to read the summary and description of the bug report and manually locate the buggy files based on this information. This manual process is often time consuming and tedious. Thus, a number of past studies have proposed bug localization techniques to automatically recover potentially buggy files from bug reports. Unfortunately, none of these techniques are integrated to bug tracking systems and thus it hinders their adoption by practitioners. To help disseminate research in bug localization to practitioners, we develop a tool named BugLocalizer, which is implemented as a Bugzilla extension and builds upon a recently proposed bug localization technique. Our tool extracts texts from summary and description fields of a bug report and source code files. It then computes similarities of the bug report with source code files to find the buggy files. Developers can use our tool online from a Bugzilla web interface by providing a link to a git source code repository and specifying the version of the repository to be analyzed. We have released our tool publicly in GitHub, which is available at: https://github.com/smagsmu/buglocalizer. We have also provided a demo video, which can be accessed at: http://youtu.be/iWHaLNCUjBY. @InProceedings{FSE14p767, author = {Ferdian Thung and Tien-Duy B. Le and Pavneet Singh Kochhar and David Lo}, title = {BugLocalizer: Integrated Tool Support for Bug Localization}, booktitle = {Proc.\ FSE}, publisher = {ACM}, pages = {767--770}, doi = {}, year = {2014}, } |
|
Le, Tien-Duy B. |
FSE '14-DEMO: "BugLocalizer: Integrated Tool ..."
BugLocalizer: Integrated Tool Support for Bug Localization
Ferdian Thung, Tien-Duy B. Le, Pavneet Singh Kochhar, and David Lo (Singapore Management University, Singapore) To manage bugs that appear in a software, developers often make use of a bug tracking system such as Bugzilla. Users can report bugs that they encounter in such a system. Whenever a user reports a new bug report, developers need to read the summary and description of the bug report and manually locate the buggy files based on this information. This manual process is often time consuming and tedious. Thus, a number of past studies have proposed bug localization techniques to automatically recover potentially buggy files from bug reports. Unfortunately, none of these techniques are integrated to bug tracking systems and thus it hinders their adoption by practitioners. To help disseminate research in bug localization to practitioners, we develop a tool named BugLocalizer, which is implemented as a Bugzilla extension and builds upon a recently proposed bug localization technique. Our tool extracts texts from summary and description fields of a bug report and source code files. It then computes similarities of the bug report with source code files to find the buggy files. Developers can use our tool online from a Bugzilla web interface by providing a link to a git source code repository and specifying the version of the repository to be analyzed. We have released our tool publicly in GitHub, which is available at: https://github.com/smagsmu/buglocalizer. We have also provided a demo video, which can be accessed at: http://youtu.be/iWHaLNCUjBY. @InProceedings{FSE14p767, author = {Ferdian Thung and Tien-Duy B. Le and Pavneet Singh Kochhar and David Lo}, title = {BugLocalizer: Integrated Tool Support for Bug Localization}, booktitle = {Proc.\ FSE}, publisher = {ACM}, pages = {767--770}, doi = {}, year = {2014}, } |
|
Li, Jianwen |
FSE '14-DEMO: "Aalta: An LTL Satisfiability ..."
Aalta: An LTL Satisfiability Checker over Infinite/Finite Traces
Jianwen Li , Yinbo Yao, Geguang Pu , Lijun Zhang, and Jifeng He (East China Normal University, China; Institute of Software at Chinese Academy of Sciences, China) Linear Temporal Logic (LTL) is been widely used nowadays in verification and AI. Checking satisfiability of LTL formulas is a fundamental step in removing possible errors in LTL assertions. We present in this paper Aalta, a new LTL satisfiability checker, which supports satisfiability checking for LTL over both infinite and finite traces. Aalta leverages the power of modern SAT solvers. We have conducted a comprehensive comparison between Aalta and other LTL satisfiability checkers, and the experimental results show that Aalta is very competitive. The tool is available at www.lab205.org/aalta. @InProceedings{FSE14p731, author = {Jianwen Li and Yinbo Yao and Geguang Pu and Lijun Zhang and Jifeng He}, title = {Aalta: An LTL Satisfiability Checker over Infinite/Finite Traces}, booktitle = {Proc.\ FSE}, publisher = {ACM}, pages = {731--734}, doi = {}, year = {2014}, } |
|
Liu, Han |
FSE '14-DEMO: "Tsmart-GalsBlock: A Toolkit ..."
Tsmart-GalsBlock: A Toolkit for Modeling, Validation, and Synthesis of Multi-clocked Embedded Systems
Yu Jiang , Hehua Zhang, Huafeng Zhang, Xinyan Zhao, Han Liu, Chengnian Sun, Xiaoyu Song, Ming Gu, and Jiaguang Sun (Tsinghua University, China; University of California at Davis, USA) The key challenges of the model-driven approach to designing multi-clocked embedded systems are three-fold: (1) how to model local synchronous components and asynchronous communication between components in a single framework, (2) how to ensure the correctness of the model, and (3) how to maintain the consistency between the model and the implementation of the system. In this paper, we present Tsmart, a self-contained toolkit to address these three challenges. Tsmart seamlessly integrates (1) a graphical editor to facilitate the modeling of the complex behaviors and structures in an embedded system, (2) a simulator for interactive graphical simulation to understand and debug the system model, (3) a verication engine to verify the correctness of the system design, and (4) a synthesis engine to automatically generate ecient executable VHDL code from the model. The toolkit has been successfully applied to designing the main control system of a train communication controller, and the system has already been deployed and in operation. The evaluation of Tsmart on this real industrial application demonstrates the eectiveness and the potential of the toolkit. @InProceedings{FSE14p711, author = {Yu Jiang and Hehua Zhang and Huafeng Zhang and Xinyan Zhao and Han Liu and Chengnian Sun and Xiaoyu Song and Ming Gu and Jiaguang Sun}, title = {Tsmart-GalsBlock: A Toolkit for Modeling, Validation, and Synthesis of Multi-clocked Embedded Systems}, booktitle = {Proc.\ FSE}, publisher = {ACM}, pages = {711--714}, doi = {}, year = {2014}, } |
|
Liu, Yang |
FSE '14-DEMO: "RaPiD: A Toolkit for Reliability ..."
RaPiD: A Toolkit for Reliability Analysis of Non-deterministic Systems
Lin Gui, Jun Sun, Yang Liu , Truong Khanh Nguyen, and Jin Song Dong (National University of Singapore, Singapore; Singapore University of Technology and Design, Singapore; Nanyang Technological University, Singapore) Non-determinism in concurrent or distributed software systems (i.e., various possible execution orders among different distributed components) presents new challenges to the existing reliability analysis methods based on Markov chains. In this work, we present a toolkit RaPiD for the reliability analysis of non-deterministic systems. Taking Markov decision process as reliability model, RaPiD can help in the analysis of three fundamental and rewarding aspects regarding software reliability. First, to have reliability assurance on a system, RaPiD can synthesize the overall system reliability given the reliability values of system components. Second, given a requirement on the overall system reliability, RaPiD can distribute the reliability requirement to each component. Lastly, RaPiD can identify the component that affects the system reliability most significantly. RaPiD has been applied to analyze several real-world systems including a financial stock trading system, a proton therapy control system and an ambient assisted living room system. @InProceedings{FSE14p727, author = {Lin Gui and Jun Sun and Yang Liu and Truong Khanh Nguyen and Jin Song Dong}, title = {RaPiD: A Toolkit for Reliability Analysis of Non-deterministic Systems}, booktitle = {Proc.\ FSE}, publisher = {ACM}, pages = {727--730}, doi = {}, year = {2014}, } Video Info |
|
Lo, David |
FSE '14-DEMO: "BugLocalizer: Integrated Tool ..."
BugLocalizer: Integrated Tool Support for Bug Localization
Ferdian Thung, Tien-Duy B. Le, Pavneet Singh Kochhar, and David Lo (Singapore Management University, Singapore) To manage bugs that appear in a software, developers often make use of a bug tracking system such as Bugzilla. Users can report bugs that they encounter in such a system. Whenever a user reports a new bug report, developers need to read the summary and description of the bug report and manually locate the buggy files based on this information. This manual process is often time consuming and tedious. Thus, a number of past studies have proposed bug localization techniques to automatically recover potentially buggy files from bug reports. Unfortunately, none of these techniques are integrated to bug tracking systems and thus it hinders their adoption by practitioners. To help disseminate research in bug localization to practitioners, we develop a tool named BugLocalizer, which is implemented as a Bugzilla extension and builds upon a recently proposed bug localization technique. Our tool extracts texts from summary and description fields of a bug report and source code files. It then computes similarities of the bug report with source code files to find the buggy files. Developers can use our tool online from a Bugzilla web interface by providing a link to a git source code repository and specifying the version of the repository to be analyzed. We have released our tool publicly in GitHub, which is available at: https://github.com/smagsmu/buglocalizer. We have also provided a demo video, which can be accessed at: http://youtu.be/iWHaLNCUjBY. @InProceedings{FSE14p767, author = {Ferdian Thung and Tien-Duy B. Le and Pavneet Singh Kochhar and David Lo}, title = {BugLocalizer: Integrated Tool Support for Bug Localization}, booktitle = {Proc.\ FSE}, publisher = {ACM}, pages = {767--770}, doi = {}, year = {2014}, } |
|
Mirakhorli, Mehdi |
FSE '14-DEMO: "Archie: A Tool for Detecting, ..."
Archie: A Tool for Detecting, Monitoring, and Preserving Architecturally Significant Code
Mehdi Mirakhorli, Ahmed Fakhry, Artem Grechko, Matteusz Wieloch, and Jane Cleland-Huang (Rochester Institute of Technology, USA; DePaul University, USA) The quality of a software architecture is largely dependent upon the underlying architectural decisions at the framework, tactic, and pattern levels. Decisions to adopt certain solutions determine the extent to which desired qualities such as security, availability, and performance are achieved in the delivered system. In this tool demo, we present our Eclipse plug-in named Archie as a solution for maintaining architectural qualities in the design and code despite long-term maintenance and evolution activities. Archie detects architectural tactics such as heartbeat, resource pooling, and role-based access control (RBAC) in the source code of a project; constructs traceability links between the tactics, design models, rationales and source code; and then uses these to monitor the environment for architecturally significant changes and to keep developers informed of underlying design decisions and their associated rationales. @InProceedings{FSE14p739, author = {Mehdi Mirakhorli and Ahmed Fakhry and Artem Grechko and Matteusz Wieloch and Jane Cleland-Huang}, title = {Archie: A Tool for Detecting, Monitoring, and Preserving Architecturally Significant Code}, booktitle = {Proc.\ FSE}, publisher = {ACM}, pages = {739--742}, doi = {}, year = {2014}, } |
|
Nguyen, Truong Khanh |
FSE '14-DEMO: "RaPiD: A Toolkit for Reliability ..."
RaPiD: A Toolkit for Reliability Analysis of Non-deterministic Systems
Lin Gui, Jun Sun, Yang Liu , Truong Khanh Nguyen, and Jin Song Dong (National University of Singapore, Singapore; Singapore University of Technology and Design, Singapore; Nanyang Technological University, Singapore) Non-determinism in concurrent or distributed software systems (i.e., various possible execution orders among different distributed components) presents new challenges to the existing reliability analysis methods based on Markov chains. In this work, we present a toolkit RaPiD for the reliability analysis of non-deterministic systems. Taking Markov decision process as reliability model, RaPiD can help in the analysis of three fundamental and rewarding aspects regarding software reliability. First, to have reliability assurance on a system, RaPiD can synthesize the overall system reliability given the reliability values of system components. Second, given a requirement on the overall system reliability, RaPiD can distribute the reliability requirement to each component. Lastly, RaPiD can identify the component that affects the system reliability most significantly. RaPiD has been applied to analyze several real-world systems including a financial stock trading system, a proton therapy control system and an ambient assisted living room system. @InProceedings{FSE14p727, author = {Lin Gui and Jun Sun and Yang Liu and Truong Khanh Nguyen and Jin Song Dong}, title = {RaPiD: A Toolkit for Reliability Analysis of Non-deterministic Systems}, booktitle = {Proc.\ FSE}, publisher = {ACM}, pages = {727--730}, doi = {}, year = {2014}, } Video Info |
|
Perucci, Alexander |
FSE '14-DEMO: "CHOReOSynt: Enforcing Choreography ..."
CHOReOSynt: Enforcing Choreography Realizability in the Future Internet
Marco Autili, Davide Di Ruscio, Amleto Di Salle, and Alexander Perucci (University of L'Aquila, Italy) Choreographies are an emergent Service Engineering (SE) approach to compose together and coordinate services in a distributed way. A choreography formalizes the way business participants coordinate their interactions. The focus is not on orchestrations of the work performed within them, but rather on the exchange of messages between these participants. The problems usually addressed when considering a choreography-based specification of the system to be realized are realizability check, and conformance check. In this paper we describe the CHOReOSynt tool, which has been conceived to deal with an additional problem, namely, automated choreography enforcement. That is, when the goal is to actually realize a service choreography by reusing third-party services, their uncontrolled (or wrongly coordinated) composite behavior may show undesired interactions that preclude the choreography realization. CHOReOSynt solves this problem by automatically synthesizing additional software entities that, when interposed among the services, allow for preventing undesired interactions. Screencast: http://choreos.disim.univaq.it/downloads/ @InProceedings{FSE14p723, author = {Marco Autili and Davide Di Ruscio and Amleto Di Salle and Alexander Perucci}, title = {CHOReOSynt: Enforcing Choreography Realizability in the Future Internet}, booktitle = {Proc.\ FSE}, publisher = {ACM}, pages = {723--726}, doi = {}, year = {2014}, } |
|
Pohlmann, Uwe |
FSE '14-DEMO: "A Tool Suite for the Model-Driven ..."
A Tool Suite for the Model-Driven Software Engineering of Cyber-Physical Systems
Stefan Dziwok, Christopher Gerking, Steffen Becker, Sebastian Thiele, Christian Heinzemann, and Uwe Pohlmann (University of Paderborn, Germany; Fraunhofer IPT, Germany) Cyber-physical systems, e.g., autonomous cars or trains, interact with their physical environment. As a consequence, they commonly have to coordinate with other systems via complex message communication while realizing safety-critical and real-time tasks. As a result, those systems should be correct by construction. Software architects can achieve this by using the MechatronicUML process and language. This paper presents the MechatronicUML Tool Suite that offers unique features to support the MechatronicUML modeling and analyses tasks. @InProceedings{FSE14p715, author = {Stefan Dziwok and Christopher Gerking and Steffen Becker and Sebastian Thiele and Christian Heinzemann and Uwe Pohlmann}, title = {A Tool Suite for the Model-Driven Software Engineering of Cyber-Physical Systems}, booktitle = {Proc.\ FSE}, publisher = {ACM}, pages = {715--718}, doi = {}, year = {2014}, } |
|
Pu, Geguang |
FSE '14-DEMO: "Aalta: An LTL Satisfiability ..."
Aalta: An LTL Satisfiability Checker over Infinite/Finite Traces
Jianwen Li , Yinbo Yao, Geguang Pu , Lijun Zhang, and Jifeng He (East China Normal University, China; Institute of Software at Chinese Academy of Sciences, China) Linear Temporal Logic (LTL) is been widely used nowadays in verification and AI. Checking satisfiability of LTL formulas is a fundamental step in removing possible errors in LTL assertions. We present in this paper Aalta, a new LTL satisfiability checker, which supports satisfiability checking for LTL over both infinite and finite traces. Aalta leverages the power of modern SAT solvers. We have conducted a comprehensive comparison between Aalta and other LTL satisfiability checkers, and the experimental results show that Aalta is very competitive. The tool is available at www.lab205.org/aalta. @InProceedings{FSE14p731, author = {Jianwen Li and Yinbo Yao and Geguang Pu and Lijun Zhang and Jifeng He}, title = {Aalta: An LTL Satisfiability Checker over Infinite/Finite Traces}, booktitle = {Proc.\ FSE}, publisher = {ACM}, pages = {731--734}, doi = {}, year = {2014}, } |
|
Ramanathan, Murali Krishna |
FSE '14-DEMO: "Omen+: A Precise Dynamic Deadlock ..."
Omen+: A Precise Dynamic Deadlock Detector for Multithreaded Java Libraries
Malavika Samak and Murali Krishna Ramanathan (Indian Institute of Science, India) Designing thread-safe libraries without concurrency defects can be a challenging task. Detecting deadlocks while invoking methods in these libraries concurrently is hard due to the possible number of method invocation combinations, the object assignments to the parameters and the associated thread interleavings. In this paper, we describe the design and implementation of OMEN+ that takes a multithreaded library as the input and detects true deadlocks in a scalable manner. We achieve this by automatically synthesizing relevant multithreaded tests and analyze the associated execution traces using a precise deadlock detector. We validate the usefulness of OMEN+ by applying it on many multithreaded Java libraries and detect a number of deadlocks even in documented thread-safe libraries. The tool is available for free download at http://www.csa.iisc.ernet.in/~sss/tool/omenplus.html. @InProceedings{FSE14p735, author = {Malavika Samak and Murali Krishna Ramanathan}, title = {Omen+: A Precise Dynamic Deadlock Detector for Multithreaded Java Libraries}, booktitle = {Proc.\ FSE}, publisher = {ACM}, pages = {735--738}, doi = {}, year = {2014}, } |
|
Samak, Malavika |
FSE '14-DEMO: "Omen+: A Precise Dynamic Deadlock ..."
Omen+: A Precise Dynamic Deadlock Detector for Multithreaded Java Libraries
Malavika Samak and Murali Krishna Ramanathan (Indian Institute of Science, India) Designing thread-safe libraries without concurrency defects can be a challenging task. Detecting deadlocks while invoking methods in these libraries concurrently is hard due to the possible number of method invocation combinations, the object assignments to the parameters and the associated thread interleavings. In this paper, we describe the design and implementation of OMEN+ that takes a multithreaded library as the input and detects true deadlocks in a scalable manner. We achieve this by automatically synthesizing relevant multithreaded tests and analyze the associated execution traces using a precise deadlock detector. We validate the usefulness of OMEN+ by applying it on many multithreaded Java libraries and detect a number of deadlocks even in documented thread-safe libraries. The tool is available for free download at http://www.csa.iisc.ernet.in/~sss/tool/omenplus.html. @InProceedings{FSE14p735, author = {Malavika Samak and Murali Krishna Ramanathan}, title = {Omen+: A Precise Dynamic Deadlock Detector for Multithreaded Java Libraries}, booktitle = {Proc.\ FSE}, publisher = {ACM}, pages = {735--738}, doi = {}, year = {2014}, } |
|
Schmitz, Peter |
FSE '14-DEMO: "Linking Sketches and Diagrams ..."
Linking Sketches and Diagrams to Source Code Artifacts
Sebastian Baltes, Peter Schmitz, and Stephan Diehl (University of Trier, Germany) Recent studies have shown that sketches and diagrams play an important role in the daily work of software developers. If these visual artifacts are archived, they are often detached from the source code they document, because there is no ad- equate tool support to assist developers in capturing, archiving, and retrieving sketches related to certain source code artifacts. This paper presents SketchLink, a tool that aims at increasing the value of sketches and diagrams created during software development by supporting developers in these tasks. Our prototype implementation provides a web application that employs the camera of smartphones and tablets to capture analog sketches, but can also be used on desktop computers to upload, for instance, computer-generated diagrams. We also implemented a plugin for a Java IDE that embeds the links in Javadoc comments and visualizes them in situ in the source code editor as graphical icons. @InProceedings{FSE14p743, author = {Sebastian Baltes and Peter Schmitz and Stephan Diehl}, title = {Linking Sketches and Diagrams to Source Code Artifacts}, booktitle = {Proc.\ FSE}, publisher = {ACM}, pages = {743--746}, doi = {}, year = {2014}, } |
|
Song, Myoungkyu |
FSE '14-DEMO: "Critics: An Interactive Code ..."
Critics: An Interactive Code Review Tool for Searching and Inspecting Systematic Changes
Tianyi Zhang, Myoungkyu Song, and Miryung Kim (University of California at Los Angeles, USA; University of Texas at Austin, USA) During peer code reviews, developers often examine program differences. When using existing program differencing tools, it is difficult for developers to inspect systematic changes—similar, related changes that are scattered across multiple files. Developers cannot easily answer questions such as "what other code locations changed similar to this change?" and "are there any other locations that are similar to this code but are not updated?" In this paper, we demonstrate Critics, an Eclipse plug-in that assists developers in inspecting systematic changes. It (1) allows developers to customize a context-aware change template, (2) searches for systematic changes using the template, and (3) detects missing or inconsistent edits. Developers can interactively refine the customized change template to see corresponding search results. Critics has potential to improve developer productivity in inspecting large, scattered edits during code reviews. The tool's demonstration video is available at https://www.youtube.com/watch?v=F2D7t_Z5rhk @InProceedings{FSE14p755, author = {Tianyi Zhang and Myoungkyu Song and Miryung Kim}, title = {Critics: An Interactive Code Review Tool for Searching and Inspecting Systematic Changes}, booktitle = {Proc.\ FSE}, publisher = {ACM}, pages = {755--758}, doi = {}, year = {2014}, } Video Info FSE '14-DEMO: "RefDistiller: A Refactoring ..." RefDistiller: A Refactoring Aware Code Review Tool for Inspecting Manual Refactoring Edits Everton L. G. Alves, Myoungkyu Song, and Miryung Kim (University of Texas at Austin, USA; Federal University of Campina Grande, Brazil; University of California at Los Angeles, USA) Manual refactoring edits are error prone, as refactoring requires developers to coordinate related transformations and understand the complex inter-relationship between affected types, methods, and variables. We present RefDistiller, a refactoring-aware code review tool that can help developers detect potential behavioral changes in manual refactoring edits. It first detects the types and locations of refactoring edits by comparing two program versions. Based on the reconstructed refactoring information, it then detects potential anomalies in refactoring edits using two techniques: (1) a template-based checker for detecting missing edits and (2) a refactoring separator for detecting extra edits that may change a program's behavior. By helping developers be aware of deviations from pure refactoring edits, RefDistiller can help developers have high confidence about the correctness of manual refactoring edits. RefDistiller is available as an Eclipse plug-in at https://sites.google.com/site/refdistiller/ and its demonstration video is available at http://youtu.be/0Iseoc5HRpU. @InProceedings{FSE14p751, author = {Everton L. G. Alves and Myoungkyu Song and Miryung Kim}, title = {RefDistiller: A Refactoring Aware Code Review Tool for Inspecting Manual Refactoring Edits}, booktitle = {Proc.\ FSE}, publisher = {ACM}, pages = {751--754}, doi = {}, year = {2014}, } |
|
Song, Xiaoyu |
FSE '14-DEMO: "Tsmart-GalsBlock: A Toolkit ..."
Tsmart-GalsBlock: A Toolkit for Modeling, Validation, and Synthesis of Multi-clocked Embedded Systems
Yu Jiang , Hehua Zhang, Huafeng Zhang, Xinyan Zhao, Han Liu, Chengnian Sun, Xiaoyu Song, Ming Gu, and Jiaguang Sun (Tsinghua University, China; University of California at Davis, USA) The key challenges of the model-driven approach to designing multi-clocked embedded systems are three-fold: (1) how to model local synchronous components and asynchronous communication between components in a single framework, (2) how to ensure the correctness of the model, and (3) how to maintain the consistency between the model and the implementation of the system. In this paper, we present Tsmart, a self-contained toolkit to address these three challenges. Tsmart seamlessly integrates (1) a graphical editor to facilitate the modeling of the complex behaviors and structures in an embedded system, (2) a simulator for interactive graphical simulation to understand and debug the system model, (3) a verication engine to verify the correctness of the system design, and (4) a synthesis engine to automatically generate ecient executable VHDL code from the model. The toolkit has been successfully applied to designing the main control system of a train communication controller, and the system has already been deployed and in operation. The evaluation of Tsmart on this real industrial application demonstrates the eectiveness and the potential of the toolkit. @InProceedings{FSE14p711, author = {Yu Jiang and Hehua Zhang and Huafeng Zhang and Xinyan Zhao and Han Liu and Chengnian Sun and Xiaoyu Song and Ming Gu and Jiaguang Sun}, title = {Tsmart-GalsBlock: A Toolkit for Modeling, Validation, and Synthesis of Multi-clocked Embedded Systems}, booktitle = {Proc.\ FSE}, publisher = {ACM}, pages = {711--714}, doi = {}, year = {2014}, } |
|
Sun, Chengnian |
FSE '14-DEMO: "Tsmart-GalsBlock: A Toolkit ..."
Tsmart-GalsBlock: A Toolkit for Modeling, Validation, and Synthesis of Multi-clocked Embedded Systems
Yu Jiang , Hehua Zhang, Huafeng Zhang, Xinyan Zhao, Han Liu, Chengnian Sun, Xiaoyu Song, Ming Gu, and Jiaguang Sun (Tsinghua University, China; University of California at Davis, USA) The key challenges of the model-driven approach to designing multi-clocked embedded systems are three-fold: (1) how to model local synchronous components and asynchronous communication between components in a single framework, (2) how to ensure the correctness of the model, and (3) how to maintain the consistency between the model and the implementation of the system. In this paper, we present Tsmart, a self-contained toolkit to address these three challenges. Tsmart seamlessly integrates (1) a graphical editor to facilitate the modeling of the complex behaviors and structures in an embedded system, (2) a simulator for interactive graphical simulation to understand and debug the system model, (3) a verication engine to verify the correctness of the system design, and (4) a synthesis engine to automatically generate ecient executable VHDL code from the model. The toolkit has been successfully applied to designing the main control system of a train communication controller, and the system has already been deployed and in operation. The evaluation of Tsmart on this real industrial application demonstrates the eectiveness and the potential of the toolkit. @InProceedings{FSE14p711, author = {Yu Jiang and Hehua Zhang and Huafeng Zhang and Xinyan Zhao and Han Liu and Chengnian Sun and Xiaoyu Song and Ming Gu and Jiaguang Sun}, title = {Tsmart-GalsBlock: A Toolkit for Modeling, Validation, and Synthesis of Multi-clocked Embedded Systems}, booktitle = {Proc.\ FSE}, publisher = {ACM}, pages = {711--714}, doi = {}, year = {2014}, } |
|
Sun, Jiaguang |
FSE '14-DEMO: "Tsmart-GalsBlock: A Toolkit ..."
Tsmart-GalsBlock: A Toolkit for Modeling, Validation, and Synthesis of Multi-clocked Embedded Systems
Yu Jiang , Hehua Zhang, Huafeng Zhang, Xinyan Zhao, Han Liu, Chengnian Sun, Xiaoyu Song, Ming Gu, and Jiaguang Sun (Tsinghua University, China; University of California at Davis, USA) The key challenges of the model-driven approach to designing multi-clocked embedded systems are three-fold: (1) how to model local synchronous components and asynchronous communication between components in a single framework, (2) how to ensure the correctness of the model, and (3) how to maintain the consistency between the model and the implementation of the system. In this paper, we present Tsmart, a self-contained toolkit to address these three challenges. Tsmart seamlessly integrates (1) a graphical editor to facilitate the modeling of the complex behaviors and structures in an embedded system, (2) a simulator for interactive graphical simulation to understand and debug the system model, (3) a verication engine to verify the correctness of the system design, and (4) a synthesis engine to automatically generate ecient executable VHDL code from the model. The toolkit has been successfully applied to designing the main control system of a train communication controller, and the system has already been deployed and in operation. The evaluation of Tsmart on this real industrial application demonstrates the eectiveness and the potential of the toolkit. @InProceedings{FSE14p711, author = {Yu Jiang and Hehua Zhang and Huafeng Zhang and Xinyan Zhao and Han Liu and Chengnian Sun and Xiaoyu Song and Ming Gu and Jiaguang Sun}, title = {Tsmart-GalsBlock: A Toolkit for Modeling, Validation, and Synthesis of Multi-clocked Embedded Systems}, booktitle = {Proc.\ FSE}, publisher = {ACM}, pages = {711--714}, doi = {}, year = {2014}, } |
|
Sun, Jun |
FSE '14-DEMO: "RaPiD: A Toolkit for Reliability ..."
RaPiD: A Toolkit for Reliability Analysis of Non-deterministic Systems
Lin Gui, Jun Sun, Yang Liu , Truong Khanh Nguyen, and Jin Song Dong (National University of Singapore, Singapore; Singapore University of Technology and Design, Singapore; Nanyang Technological University, Singapore) Non-determinism in concurrent or distributed software systems (i.e., various possible execution orders among different distributed components) presents new challenges to the existing reliability analysis methods based on Markov chains. In this work, we present a toolkit RaPiD for the reliability analysis of non-deterministic systems. Taking Markov decision process as reliability model, RaPiD can help in the analysis of three fundamental and rewarding aspects regarding software reliability. First, to have reliability assurance on a system, RaPiD can synthesize the overall system reliability given the reliability values of system components. Second, given a requirement on the overall system reliability, RaPiD can distribute the reliability requirement to each component. Lastly, RaPiD can identify the component that affects the system reliability most significantly. RaPiD has been applied to analyze several real-world systems including a financial stock trading system, a proton therapy control system and an ambient assisted living room system. @InProceedings{FSE14p727, author = {Lin Gui and Jun Sun and Yang Liu and Truong Khanh Nguyen and Jin Song Dong}, title = {RaPiD: A Toolkit for Reliability Analysis of Non-deterministic Systems}, booktitle = {Proc.\ FSE}, publisher = {ACM}, pages = {727--730}, doi = {}, year = {2014}, } Video Info |
|
Thiele, Sebastian |
FSE '14-DEMO: "A Tool Suite for the Model-Driven ..."
A Tool Suite for the Model-Driven Software Engineering of Cyber-Physical Systems
Stefan Dziwok, Christopher Gerking, Steffen Becker, Sebastian Thiele, Christian Heinzemann, and Uwe Pohlmann (University of Paderborn, Germany; Fraunhofer IPT, Germany) Cyber-physical systems, e.g., autonomous cars or trains, interact with their physical environment. As a consequence, they commonly have to coordinate with other systems via complex message communication while realizing safety-critical and real-time tasks. As a result, those systems should be correct by construction. Software architects can achieve this by using the MechatronicUML process and language. This paper presents the MechatronicUML Tool Suite that offers unique features to support the MechatronicUML modeling and analyses tasks. @InProceedings{FSE14p715, author = {Stefan Dziwok and Christopher Gerking and Steffen Becker and Sebastian Thiele and Christian Heinzemann and Uwe Pohlmann}, title = {A Tool Suite for the Model-Driven Software Engineering of Cyber-Physical Systems}, booktitle = {Proc.\ FSE}, publisher = {ACM}, pages = {715--718}, doi = {}, year = {2014}, } |
|
Thung, Ferdian |
FSE '14-DEMO: "BugLocalizer: Integrated Tool ..."
BugLocalizer: Integrated Tool Support for Bug Localization
Ferdian Thung, Tien-Duy B. Le, Pavneet Singh Kochhar, and David Lo (Singapore Management University, Singapore) To manage bugs that appear in a software, developers often make use of a bug tracking system such as Bugzilla. Users can report bugs that they encounter in such a system. Whenever a user reports a new bug report, developers need to read the summary and description of the bug report and manually locate the buggy files based on this information. This manual process is often time consuming and tedious. Thus, a number of past studies have proposed bug localization techniques to automatically recover potentially buggy files from bug reports. Unfortunately, none of these techniques are integrated to bug tracking systems and thus it hinders their adoption by practitioners. To help disseminate research in bug localization to practitioners, we develop a tool named BugLocalizer, which is implemented as a Bugzilla extension and builds upon a recently proposed bug localization technique. Our tool extracts texts from summary and description fields of a bug report and source code files. It then computes similarities of the bug report with source code files to find the buggy files. Developers can use our tool online from a Bugzilla web interface by providing a link to a git source code repository and specifying the version of the repository to be analyzed. We have released our tool publicly in GitHub, which is available at: https://github.com/smagsmu/buglocalizer. We have also provided a demo video, which can be accessed at: http://youtu.be/iWHaLNCUjBY. @InProceedings{FSE14p767, author = {Ferdian Thung and Tien-Duy B. Le and Pavneet Singh Kochhar and David Lo}, title = {BugLocalizer: Integrated Tool Support for Bug Localization}, booktitle = {Proc.\ FSE}, publisher = {ACM}, pages = {767--770}, doi = {}, year = {2014}, } |
|
Wieloch, Matteusz |
FSE '14-DEMO: "Archie: A Tool for Detecting, ..."
Archie: A Tool for Detecting, Monitoring, and Preserving Architecturally Significant Code
Mehdi Mirakhorli, Ahmed Fakhry, Artem Grechko, Matteusz Wieloch, and Jane Cleland-Huang (Rochester Institute of Technology, USA; DePaul University, USA) The quality of a software architecture is largely dependent upon the underlying architectural decisions at the framework, tactic, and pattern levels. Decisions to adopt certain solutions determine the extent to which desired qualities such as security, availability, and performance are achieved in the delivered system. In this tool demo, we present our Eclipse plug-in named Archie as a solution for maintaining architectural qualities in the design and code despite long-term maintenance and evolution activities. Archie detects architectural tactics such as heartbeat, resource pooling, and role-based access control (RBAC) in the source code of a project; constructs traceability links between the tactics, design models, rationales and source code; and then uses these to monitor the environment for architecturally significant changes and to keep developers informed of underlying design decisions and their associated rationales. @InProceedings{FSE14p739, author = {Mehdi Mirakhorli and Ahmed Fakhry and Artem Grechko and Matteusz Wieloch and Jane Cleland-Huang}, title = {Archie: A Tool for Detecting, Monitoring, and Preserving Architecturally Significant Code}, booktitle = {Proc.\ FSE}, publisher = {ACM}, pages = {739--742}, doi = {}, year = {2014}, } |
|
Xiao, Lu |
FSE '14-DEMO: "Titan: A Toolset That Connects ..."
Titan: A Toolset That Connects Software Architecture with Quality Analysis
Lu Xiao, Yuanfang Cai, and Rick Kazman (Drexel University, USA; University of Hawaii, USA) In this tool demo, we will illustrate our tool---Titan---that supports a new architecture model: design rule spaces (DRSpaces). We will show how Titan can capture both architecture and evolutionary structure and help to bridge the gap between architecture and defect prediction. We will demo how to use our toolset to capture hundreds of buggy files into just a few architecturally related groups, and to reveal architecture issues that contribute to the error-proneness and change-proneness of these groups. Our tool has been used to analyze dozens of large-scale industrial projects, and has demonstrated its ability to provide valuable direction on which parts of the architecture are problematic, and on why, when, and how to refactor. The video demo of Titan can be found at https://art.cs.drexel.edu/~lx52/titan.mp4 @InProceedings{FSE14p763, author = {Lu Xiao and Yuanfang Cai and Rick Kazman}, title = {Titan: A Toolset That Connects Software Architecture with Quality Analysis}, booktitle = {Proc.\ FSE}, publisher = {ACM}, pages = {763--766}, doi = {}, year = {2014}, } |
|
Yao, Yinbo |
FSE '14-DEMO: "Aalta: An LTL Satisfiability ..."
Aalta: An LTL Satisfiability Checker over Infinite/Finite Traces
Jianwen Li , Yinbo Yao, Geguang Pu , Lijun Zhang, and Jifeng He (East China Normal University, China; Institute of Software at Chinese Academy of Sciences, China) Linear Temporal Logic (LTL) is been widely used nowadays in verification and AI. Checking satisfiability of LTL formulas is a fundamental step in removing possible errors in LTL assertions. We present in this paper Aalta, a new LTL satisfiability checker, which supports satisfiability checking for LTL over both infinite and finite traces. Aalta leverages the power of modern SAT solvers. We have conducted a comprehensive comparison between Aalta and other LTL satisfiability checkers, and the experimental results show that Aalta is very competitive. The tool is available at www.lab205.org/aalta. @InProceedings{FSE14p731, author = {Jianwen Li and Yinbo Yao and Geguang Pu and Lijun Zhang and Jifeng He}, title = {Aalta: An LTL Satisfiability Checker over Infinite/Finite Traces}, booktitle = {Proc.\ FSE}, publisher = {ACM}, pages = {731--734}, doi = {}, year = {2014}, } |
|
Zeller, Andreas |
FSE '14-DEMO: "XMLMate: Evolutionary XML ..."
XMLMate: Evolutionary XML Test Generation
Nikolas Havrikov, Matthias Höschele, Juan Pablo Galeotti, and Andreas Zeller (Saarland University, Germany) Generating system inputs satisfying complex constraints is still a challenge for modern test generators. We present XMLMATE, a search-based test generator specially aimed at XML-based systems. XMLMATE leverages program structure, existing XML schemas, and XML inputs to generate, mutate, recombine, and evolve valid XML inputs. Over a set of seven XML-based systems, XMLMATE detected 31 new unique failures in production code, all triggered by system inputs and thus true alarms. @InProceedings{FSE14p719, author = {Nikolas Havrikov and Matthias Höschele and Juan Pablo Galeotti and Andreas Zeller}, title = {XMLMate: Evolutionary XML Test Generation}, booktitle = {Proc.\ FSE}, publisher = {ACM}, pages = {719--722}, doi = {}, year = {2014}, } Video Info |
|
Zhang, Hehua |
FSE '14-DEMO: "Tsmart-GalsBlock: A Toolkit ..."
Tsmart-GalsBlock: A Toolkit for Modeling, Validation, and Synthesis of Multi-clocked Embedded Systems
Yu Jiang , Hehua Zhang, Huafeng Zhang, Xinyan Zhao, Han Liu, Chengnian Sun, Xiaoyu Song, Ming Gu, and Jiaguang Sun (Tsinghua University, China; University of California at Davis, USA) The key challenges of the model-driven approach to designing multi-clocked embedded systems are three-fold: (1) how to model local synchronous components and asynchronous communication between components in a single framework, (2) how to ensure the correctness of the model, and (3) how to maintain the consistency between the model and the implementation of the system. In this paper, we present Tsmart, a self-contained toolkit to address these three challenges. Tsmart seamlessly integrates (1) a graphical editor to facilitate the modeling of the complex behaviors and structures in an embedded system, (2) a simulator for interactive graphical simulation to understand and debug the system model, (3) a verication engine to verify the correctness of the system design, and (4) a synthesis engine to automatically generate ecient executable VHDL code from the model. The toolkit has been successfully applied to designing the main control system of a train communication controller, and the system has already been deployed and in operation. The evaluation of Tsmart on this real industrial application demonstrates the eectiveness and the potential of the toolkit. @InProceedings{FSE14p711, author = {Yu Jiang and Hehua Zhang and Huafeng Zhang and Xinyan Zhao and Han Liu and Chengnian Sun and Xiaoyu Song and Ming Gu and Jiaguang Sun}, title = {Tsmart-GalsBlock: A Toolkit for Modeling, Validation, and Synthesis of Multi-clocked Embedded Systems}, booktitle = {Proc.\ FSE}, publisher = {ACM}, pages = {711--714}, doi = {}, year = {2014}, } |
|
Zhang, Huafeng |
FSE '14-DEMO: "Tsmart-GalsBlock: A Toolkit ..."
Tsmart-GalsBlock: A Toolkit for Modeling, Validation, and Synthesis of Multi-clocked Embedded Systems
Yu Jiang , Hehua Zhang, Huafeng Zhang, Xinyan Zhao, Han Liu, Chengnian Sun, Xiaoyu Song, Ming Gu, and Jiaguang Sun (Tsinghua University, China; University of California at Davis, USA) The key challenges of the model-driven approach to designing multi-clocked embedded systems are three-fold: (1) how to model local synchronous components and asynchronous communication between components in a single framework, (2) how to ensure the correctness of the model, and (3) how to maintain the consistency between the model and the implementation of the system. In this paper, we present Tsmart, a self-contained toolkit to address these three challenges. Tsmart seamlessly integrates (1) a graphical editor to facilitate the modeling of the complex behaviors and structures in an embedded system, (2) a simulator for interactive graphical simulation to understand and debug the system model, (3) a verication engine to verify the correctness of the system design, and (4) a synthesis engine to automatically generate ecient executable VHDL code from the model. The toolkit has been successfully applied to designing the main control system of a train communication controller, and the system has already been deployed and in operation. The evaluation of Tsmart on this real industrial application demonstrates the eectiveness and the potential of the toolkit. @InProceedings{FSE14p711, author = {Yu Jiang and Hehua Zhang and Huafeng Zhang and Xinyan Zhao and Han Liu and Chengnian Sun and Xiaoyu Song and Ming Gu and Jiaguang Sun}, title = {Tsmart-GalsBlock: A Toolkit for Modeling, Validation, and Synthesis of Multi-clocked Embedded Systems}, booktitle = {Proc.\ FSE}, publisher = {ACM}, pages = {711--714}, doi = {}, year = {2014}, } |
|
Zhang, Lijun |
FSE '14-DEMO: "Aalta: An LTL Satisfiability ..."
Aalta: An LTL Satisfiability Checker over Infinite/Finite Traces
Jianwen Li , Yinbo Yao, Geguang Pu , Lijun Zhang, and Jifeng He (East China Normal University, China; Institute of Software at Chinese Academy of Sciences, China) Linear Temporal Logic (LTL) is been widely used nowadays in verification and AI. Checking satisfiability of LTL formulas is a fundamental step in removing possible errors in LTL assertions. We present in this paper Aalta, a new LTL satisfiability checker, which supports satisfiability checking for LTL over both infinite and finite traces. Aalta leverages the power of modern SAT solvers. We have conducted a comprehensive comparison between Aalta and other LTL satisfiability checkers, and the experimental results show that Aalta is very competitive. The tool is available at www.lab205.org/aalta. @InProceedings{FSE14p731, author = {Jianwen Li and Yinbo Yao and Geguang Pu and Lijun Zhang and Jifeng He}, title = {Aalta: An LTL Satisfiability Checker over Infinite/Finite Traces}, booktitle = {Proc.\ FSE}, publisher = {ACM}, pages = {731--734}, doi = {}, year = {2014}, } |
|
Zhang, Tianyi |
FSE '14-DEMO: "Critics: An Interactive Code ..."
Critics: An Interactive Code Review Tool for Searching and Inspecting Systematic Changes
Tianyi Zhang, Myoungkyu Song, and Miryung Kim (University of California at Los Angeles, USA; University of Texas at Austin, USA) During peer code reviews, developers often examine program differences. When using existing program differencing tools, it is difficult for developers to inspect systematic changes—similar, related changes that are scattered across multiple files. Developers cannot easily answer questions such as "what other code locations changed similar to this change?" and "are there any other locations that are similar to this code but are not updated?" In this paper, we demonstrate Critics, an Eclipse plug-in that assists developers in inspecting systematic changes. It (1) allows developers to customize a context-aware change template, (2) searches for systematic changes using the template, and (3) detects missing or inconsistent edits. Developers can interactively refine the customized change template to see corresponding search results. Critics has potential to improve developer productivity in inspecting large, scattered edits during code reviews. The tool's demonstration video is available at https://www.youtube.com/watch?v=F2D7t_Z5rhk @InProceedings{FSE14p755, author = {Tianyi Zhang and Myoungkyu Song and Miryung Kim}, title = {Critics: An Interactive Code Review Tool for Searching and Inspecting Systematic Changes}, booktitle = {Proc.\ FSE}, publisher = {ACM}, pages = {755--758}, doi = {}, year = {2014}, } Video Info |
|
Zhao, Xinyan |
FSE '14-DEMO: "Tsmart-GalsBlock: A Toolkit ..."
Tsmart-GalsBlock: A Toolkit for Modeling, Validation, and Synthesis of Multi-clocked Embedded Systems
Yu Jiang , Hehua Zhang, Huafeng Zhang, Xinyan Zhao, Han Liu, Chengnian Sun, Xiaoyu Song, Ming Gu, and Jiaguang Sun (Tsinghua University, China; University of California at Davis, USA) The key challenges of the model-driven approach to designing multi-clocked embedded systems are three-fold: (1) how to model local synchronous components and asynchronous communication between components in a single framework, (2) how to ensure the correctness of the model, and (3) how to maintain the consistency between the model and the implementation of the system. In this paper, we present Tsmart, a self-contained toolkit to address these three challenges. Tsmart seamlessly integrates (1) a graphical editor to facilitate the modeling of the complex behaviors and structures in an embedded system, (2) a simulator for interactive graphical simulation to understand and debug the system model, (3) a verication engine to verify the correctness of the system design, and (4) a synthesis engine to automatically generate ecient executable VHDL code from the model. The toolkit has been successfully applied to designing the main control system of a train communication controller, and the system has already been deployed and in operation. The evaluation of Tsmart on this real industrial application demonstrates the eectiveness and the potential of the toolkit. @InProceedings{FSE14p711, author = {Yu Jiang and Hehua Zhang and Huafeng Zhang and Xinyan Zhao and Han Liu and Chengnian Sun and Xiaoyu Song and Ming Gu and Jiaguang Sun}, title = {Tsmart-GalsBlock: A Toolkit for Modeling, Validation, and Synthesis of Multi-clocked Embedded Systems}, booktitle = {Proc.\ FSE}, publisher = {ACM}, pages = {711--714}, doi = {}, year = {2014}, } |
58 authors
proc time: 1.11