Testing object-oriented programs is still a hard task, despite many studies on criteria to better cover the test space. Test criteria establish requirements one want to achieve in testing programs to help in finding s...
详细信息
ISBN:
(纸本)9781595937537
Testing object-oriented programs is still a hard task, despite many studies on criteria to better cover the test space. Test criteria establish requirements one want to achieve in testing programs to help in finding software defects. On the other hand, program verification guarantees that a program preserves its specification but it is not very straightforwardly applicable in many cases. Both program testing and verification axe expensive tasks and could be used to complement each other. This paper presents a study on using formal verification to reduce the space of program testing. As properties are checked using program model checkers, programs are traced. Information from these traces can be used to realize how much testing criteria have been satisfied, reducing the further program test space. The present work is a study on how much the test space of concurrent java programs can be reduced if DeadlockFreedom is checked prior to testing.
The main limitation of software model checking is that, due to state explosion, it does not scale to real-world multi-threaded programs. One of the reasons is that current software model checkers adhere to full semant...
详细信息
ISBN:
(纸本)9783642045691
The main limitation of software model checking is that, due to state explosion, it does not scale to real-world multi-threaded programs. One of the reasons is that current software model checkers adhere to full semantics of programming languages, which are based on very permissive models of concurrency. Current runtime platforms for programs, however, restrict concurrency in various ways - it is visible especially in the case of critical embedded systems, which typically involve only a single processor and use a threading model based on limited preemption. In this paper, we present a technique for addressing state explosion in model checking of java programs for embedded systems, which exploits restrictions on concurrency common to current java platforms for such systems. We have implemented the technique in java PathFinder and performed a number of experiments on Purdue Collision Detector, which is a non-trivial multi-threaded java program. Results of experiments show that use of the restrictions on concurrency in model checking with java Path Finder reduces the state space size by an order of magnitude and also reduces the time needed to discover errors in java programs.
The size of the test suite and the duration of time determines the time taken by the regression testing. Conversely, the testers can prioritise the test cases by the use of a competent prioritisation technique to obta...
详细信息
The size of the test suite and the duration of time determines the time taken by the regression testing. Conversely, the testers can prioritise the test cases by the use of a competent prioritisation technique to obtain an increased rate of fault detection in the system, allowing for earlier corrections, and getting higher overall confidence that the software has been tested suitably. A prioritised test suite is more likely to be more effective during that time period than would have been achieved via a random ordering if execution needs to be suspended after some time. An enhanced test case ordering may be probable if the desired implementation time to run the test cases is proven earlier. This research work's main intention is to prioritise the regression-testing test cases. In order to prioritise the test cases some factors are considered here. These factors are employed in the prioritisation algorithm. The trace events are one of the important factors, used to find the most significant test cases in the projects. The requirement factor value is calculated and subsequently a weightage is calculated and assigned to each test case in the software based on these factors by using a thresholding technique. Later, the test cases are prioritised according to the weightage allocated to them. Executing the test cases based on the prioritisation will greatly decreases the computation cost and time. The proposed technique is efficient in prioritising the regression test cases. The new prioritised subsequences of the given unit test suites are executed on java programs after the completion of prioritisation. Average of the percentage of faults detected is an evaluation metric used for evaluating the 'superiority' of these orderings.
Despite garbage collectors, programmers must manually manage many non-memory finite system resources' such as file descriptors and database connections. Unreleased resources result in resource leaks' that degr...
详细信息
Despite garbage collectors, programmers must manually manage many non-memory finite system resources' such as file descriptors and database connections. Unreleased resources result in resource leaks' that degrade application performance and can even result in system crashes. It is hard to test resource leaks because of their no immediate symptoms in the short run. There are analysis techniques to detect resource leaks statically or dynamically. However, all of them require the formal specification as input, which seriously decrease their practicability for common software developers. In this study, the authors propose an easy-to-use yet effective resource leak testing approach for java programs based on existing finalisers of java Application Programming Interface (API) classes. They instrument resource classes to check that the cleanup method of a resource object is called before its finaliser's execution. Otherwise, this resource object is leaked. To use this approach, programmers just add a few lines of code into their programs and no formal specifications are required. They carry out experiments on benchmarks in the literature to evaluate the incidence of object finalisation and performance cost of finalisers. Experimental results show that the authors' approach can test leaks of most system resources with high effectiveness and low overhead.
University Health Network (UHN) Pathology, in its capacity of providing neuro-oncologic care, now utilizes a laboratory information system ( LIS), which was instituted in September 2001. For the 75 years preceding the...
详细信息
University Health Network (UHN) Pathology, in its capacity of providing neuro-oncologic care, now utilizes a laboratory information system ( LIS), which was instituted in September 2001. For the 75 years preceding the LIS, more than 50 000 pathology reports exist in paper format. High-throughput automated scanning of the paper archives was employed to add the most recent 30 years of paper records (30 000 neuropathology specimens) to the LIS. The searchable portable document format (PDF) files generated from the scans were filtered through a multi-tiered process driven by java computer programs that selected relevant patient and diagnostic information. A second series of programs queried the neuropathologist-assigned diagnoses and successfully converted these to the standardized World Health Organization (WHO) format. This was achieved with a master list of key site and diagnostic terms, and prioritization rules that were determined on a trial and error basis. Categorization, verification, and consolidation were completed within 3 months and on a C$10 000 budget.
Perpetrators might employ computer programs (software) to perform their offenses or to cover their wrongdoings. Program's source code, in particular variables and their values diverge in their scope and duration i...
详细信息
ISBN:
(纸本)9781538637319
Perpetrators might employ computer programs (software) to perform their offenses or to cover their wrongdoings. Program's source code, in particular variables and their values diverge in their scope and duration in RAM. Object oriented languages encapsulate variables and operations in classes and allow for objects to be instantiated, which simplify software design but add to the complexity of its execution behavior and its data and control flow. This paper explores execution behaviors and information left by program execution in support for legal actions against perpetrators in the court of law. Our investigation model assumes no information is provided by the operating system;only raw RAM dumps. Our methodology employs information from the presumed program source code and its object oriented design. It explores various execution states and scenarios to uncover the evidence of potential software usage. These scenarios are designed to show that scope, access modifiers, and storage information of various source code variables can be used to identify program's activities. Results show that investigators have good chances locating various variables' values that are uniquely corresponded to the presumed software and its execution states. In some cases, values are successfully identified in memory dumps even after the process is stopped.
The use of computer-based systems has increased significantly over the last years in several domains, mainly when we take into account the applications running on mobile platforms that have exploded in just a few shor...
详细信息
ISBN:
(纸本)9781509026531
The use of computer-based systems has increased significantly over the last years in several domains, mainly when we take into account the applications running on mobile platforms that have exploded in just a few short years, so that software verification and testing now play an important role in ensuring the overall product quality. In this paper, we describe the preliminary results of a work that presents a method to integrate formal verification techniques adopting ESC/java2 and JCute tools with unit testing by TestNG framework to verify java programs. This method aims to extract the safety properties generated by ESC/java2 to automatically generate test cases using the rich set of assertions provided by the TestNG framework and JCute to validate those test cases. It is worth noting that is widely recognized that there is a growing need for automated testing techniques aimed at mobile applications, in platforms, such as: Android or java Platform, Micro Edition (java ME). Additionally, a critical challenge is the systematic generation of test cases. We show preliminary results of our proposed method over publicly available benchmarks, and compare the results to recognized tools, e.g., CBMC and javaPathFinder. Experimental results show that our proposed method detects 86.04% of correct results (i.e., if a property satisfy its specification or is violated), while CBMC has found 79.06%, and JPF has found 93, 02%.
We present Bugs. jar, a large-scale dataset for research in automated debugging, patching, and testing of java programs. Bugs. jar is comprised of 1,158 bugs and patches, drawn from 8 large, popular open-source java p...
详细信息
ISBN:
(纸本)9781450357166
We present Bugs. jar, a large-scale dataset for research in automated debugging, patching, and testing of java programs. Bugs. jar is comprised of 1,158 bugs and patches, drawn from 8 large, popular open-source java projects, spanning 8 diverse and prominent application categories. It is an order of magnitude larger than Defects4J, the only other dataset in its class. We discuss the methodology used for constructing Bugs. jar, the representation of the dataset, several use-cases, and an illustration of three of the use-cases through the application of 3 specific tools on Bugs. jar, namely our own tool, Elixir, and two third-party tools, Ekstazi and JaCoCo.
This paper presents a strategy for the visualization of dynamic object relationships in java programs. The metaphor of a chemical molecule is used to aid Comprehension, and to help in reducing the size of the object g...
详细信息
ISBN:
(纸本)0769524435
This paper presents a strategy for the visualization of dynamic object relationships in java programs. The metaphor of a chemical molecule is used to aid Comprehension, and to help in reducing the size of the object graph. Our strategy has been implemented by dynamically instrumenting java bytecode to collect trace data, which is then analyzed and visualized in 3D using VRML. Quantitative and graphical results are presented, based on an analysis of programs in the SPEC JVM98 and JOlden benchmark suites.
A unique book-and-video package presented by java guru Yakov Fain As one of the most popular software languages for building Web applications, java is often the first programming language developers learn. The latest ...
详细信息
ISBN:
(数字)9781118058176
ISBN:
(纸本)9780470889640
A unique book-and-video package presented by java guru Yakov Fain As one of the most popular software languages for building Web applications, java is often the first programming language developers learn. The latest version includes numerous updates that both novice and experienced developers need to know. With this invaluable book-and-video package, java authority Yakov Fain fully covers java?s new features as well as its language extensions, classes and class methods, and the Swing Application Framework. For each lesson that he discusses in the book, there is an accompanying instructional video to reinforce your learning *** include:Introducing java Eclipse IDE Object-Oriented Programming Class MethodsBack to java Basics Packages, Interfaces, and Encapsulation Programming with Abstract Classes and InterfacesIntroducing the Graphic User InterfaceEvent Handling in UIIntroduction to java Applets Developing a Tic-Tac-Toe Applet Developing a Ping-Pong Game Error Handling Introduction to Collections Introduction to Generics Working with Streams java Serialization Network ProgrammingProcessing E-Mails with java Introduction to Multi-Threading Digging Deeper into Concurrent Execution Working with Databases Using JDBC Swing with JTable Annotations and Reflection Remote Method Invocation java EE 6 Overview Programming with Servlets javaServer Pages Developing Web Applications with JSF Introducing JMS and MOM Introducing JNDIIntroduction to Enterprise javaBeansIntroduction to the java Persistence APIWorking with RESTful Web ServicesIntroduction to Spring MVC Framework Introduction to Hibernate Framework Bringing javaFX to the Mix java Technical Interviews Note: As part of the print version of this title, video lessons are included on DVD. For e-book versions, video lessons can be accessed at *** using a link provided in the interior of the e-book.?
暂无评论