ISSTA 2013 – Author Index |
Contents -
Abstracts -
Authors
|
Bonacchi, Andrea |
ISSTA '13-DOCTORAL: "Formal Safety Proof: A Real ..."
Formal Safety Proof: A Real Case Study in a Railway Interlocking System
Andrea Bonacchi (University of Florence, Italy) A challenging problem for model checking is represented by railway interlocking systems. It is a well known fact that interlocking systems, due to their inherent complexity related to the high number of variables involved, are not readily amenable to automatic verification, typically incurring in state space explosion problems. The study described in this paper aims at evaluating and experimenting the industrial application of verification by model checking for this class of systems. The choices made at the beginning of the study, also on the basis of specific requirements from the industrial partner, are presented, together with the advancement status of the project and the plans for its completion. @InProceedings{ISSTA13p378, author = {Andrea Bonacchi}, title = {Formal Safety Proof: A Real Case Study in a Railway Interlocking System}, booktitle = {Proc.\ ISSTA}, publisher = {ACM}, pages = {378--381}, doi = {}, year = {2013}, } |
|
Buda, Teodora Sandra |
ISSTA '13-DOCTORAL: "Generation of Test Databases ..."
Generation of Test Databases using Sampling Methods
Teodora Sandra Buda (University College Dublin, Ireland) Populating the testing environment with relevant data represents a great challenge in software validation, generally requiring expert knowledge about the system under development, as its data critically impacts the outcome of the tests designed to assess the system. Current practices of populating the testing environments generally focus on developing efficient algorithms for generating synthetic data or use the production environment for testing purposes. The latter is an invaluable strategy to provide real test cases in order to discover issues that critically impact the user of the system. However, the production environment generally consists of large amounts of data that are difficult to handle and analyze. Database sampling from the production environment is a potential solution to overcome these challenges. In this research, we propose two database sampling methods, VFDS and CoDS, with the objective of populating the testing environment. The first method is a very fast random sampling approach, while the latter aims at preserving the distribution of data in order to produce a representative sample. In particular, we focus on the dependencies between the data from different tables and the method tries to preserve the distributions of these dependencies. @InProceedings{ISSTA13p366, author = {Teodora Sandra Buda}, title = {Generation of Test Databases using Sampling Methods}, booktitle = {Proc.\ ISSTA}, publisher = {ACM}, pages = {366--369}, doi = {}, year = {2013}, } |
|
De Melo, Ana C. V. |
ISSTA '13-DOCTORAL: "Generation of Java Programs ..."
Generation of Java Programs Properties from Test Purposes
Simone Hanazumi and Ana C. V. de Melo (USP, Brazil) Software formal verification is a technique used to ensure that computational systems have high-quality and work properly. From the system specification described in a formal language, we define properties that must be satisfied during system execution to guarantee the software quality. Then, these properties should be implemented in a verifier, tool responsible for running the verification and for notifying which properties were satisfied or not. When the verification process finishes, the verifier will indicate to software developers the possible location of each code fault in the system. The disadvantages of using formal verification are the high cost to apply this technique in real systems, and the necessity of having people with experience in formal languages and formal methods. In addition, the implementation of properties related to a particular system in a verifier is a complex task. To help software developers in the application of formal verification in Java programs, this work proposes the generation of properties code, for direct use in a verifier, from test purposes derived from system formal requirements. @InProceedings{ISSTA13p362, author = {Simone Hanazumi and Ana C. V. de Melo}, title = {Generation of Java Programs Properties from Test Purposes}, booktitle = {Proc.\ ISSTA}, publisher = {ACM}, pages = {362--365}, doi = {}, year = {2013}, } |
|
Ghaith, Shadi |
ISSTA '13-DOCTORAL: "Analysis of Performance Regression ..."
Analysis of Performance Regression Testing Data by Transaction Profiles
Shadi Ghaith (University College Dublin, Ireland) Performance regression testing is an important step in the software development lifecycle, especially for enterprise applications. Commonly the analysis of performance regression testing to find anomalies is carried out manually and therefore can be error-prone, time consuming and sensitive to the input load. In our research, we propose a new technique that overcomes the above problems which helps the performance testing teams to improve their process and speeds up the entire software production process. @InProceedings{ISSTA13p370, author = {Shadi Ghaith}, title = {Analysis of Performance Regression Testing Data by Transaction Profiles}, booktitle = {Proc.\ ISSTA}, publisher = {ACM}, pages = {370--373}, doi = {}, year = {2013}, } |
|
Hanazumi, Simone |
ISSTA '13-DOCTORAL: "Generation of Java Programs ..."
Generation of Java Programs Properties from Test Purposes
Simone Hanazumi and Ana C. V. de Melo (USP, Brazil) Software formal verification is a technique used to ensure that computational systems have high-quality and work properly. From the system specification described in a formal language, we define properties that must be satisfied during system execution to guarantee the software quality. Then, these properties should be implemented in a verifier, tool responsible for running the verification and for notifying which properties were satisfied or not. When the verification process finishes, the verifier will indicate to software developers the possible location of each code fault in the system. The disadvantages of using formal verification are the high cost to apply this technique in real systems, and the necessity of having people with experience in formal languages and formal methods. In addition, the implementation of properties related to a particular system in a verifier is a complex task. To help software developers in the application of formal verification in Java programs, this work proposes the generation of properties code, for direct use in a verifier, from test purposes derived from system formal requirements. @InProceedings{ISSTA13p362, author = {Simone Hanazumi and Ana C. V. de Melo}, title = {Generation of Java Programs Properties from Test Purposes}, booktitle = {Proc.\ ISSTA}, publisher = {ACM}, pages = {362--365}, doi = {}, year = {2013}, } |
|
Park, Sangmin |
ISSTA '13-DOCTORAL: "Debugging Non-deadlock Concurrency ..."
Debugging Non-deadlock Concurrency Bugs
Sangmin Park (Georgia Tech, USA) Concurrency bugs are difficult to debug because of nondeterministic behaviors of concurrent programs. Existing fault-localization techniques for non-deadlock concurrency bugs do not provide the comprehensive information to identify and understand the bugs. Existing automatic fault-fix techniques for concurrency bugs do not provide confidence that the fault has been fixed. To address the limitations of existing techniques, this research will develop techniques that will assist developers in several aspects of debugging, from finding the locations of concurrency bugs to providing confidence after the fix. The expected contributions of this research include a fault-localization technique that locates concurrency bugs, a fault-comprehension technique that assists understanding of bugs, a fix-confidence technique that provides confidence of fixes, and a framework that implements the techniques and that is used to perform empirical studies to evaluate the techniques. @InProceedings{ISSTA13p358, author = {Sangmin Park}, title = {Debugging Non-deadlock Concurrency Bugs}, booktitle = {Proc.\ ISSTA}, publisher = {ACM}, pages = {358--361}, doi = {}, year = {2013}, } |
|
Thüm, Thomas |
ISSTA '13-DOCTORAL: "Product-Line Verification ..."
Product-Line Verification with Feature-Oriented Contracts
Thomas Thüm (University of Magdeburg, Germany) Software product lines allow programmers to reuse code across similar software products. Software products are decomposed into separate modules representing user-visible features. Based on a selection of desired features, a customized software product can be generated automatically. However, these reuse mechanisms challenge existing techniques for specification and verification of software. Specifying and verifying each product involves redundant steps, and is often infeasible. We discuss how method contracts (i.e., preconditions and postconditions) can be used to efficiently specify and verify product lines. @InProceedings{ISSTA13p374, author = {Thomas Thüm}, title = {Product-Line Verification with Feature-Oriented Contracts}, booktitle = {Proc.\ ISSTA}, publisher = {ACM}, pages = {374--377}, doi = {}, year = {2013}, } Info |
7 authors
proc time: 1.07