We present a new machine-learning algorithm with disjunctive model for data-driven program analysis. One major challenge in static program analysis is a substantial amount of manual effort required for tuning the analysis performance. Recently, data-driven program analysis has emerged to address this challenge by automatically adjusting the analysis based on data through a learning algorithm. Although this new approach has proven promising for various program analysis tasks, its effectiveness has been limited due to simple-minded learning models and algorithms that are unable to capture sophisticated, in particular disjunctive, program properties. To overcome this shortcoming, this article presents a new disjunctive model for data-driven program analysis as well as a learning algorithm to find the model parameters. Our model uses Boolean formulas over atomic features and therefore is able to express nonlinear combinations of program properties. A key technical challenge is to efficiently determine a set of good Boolean formulas, as brute-force search would simply be impractical. We present a stepwise and greedy algorithm that efficiently learns Boolean formulas. We show the effectiveness and generality of our algorithm with two static analyzers: context-sensitive points-to analysis for Java and flow-sensitive interval analysis for C. Experimental results show that our automated technique significantly improves the performance of the state-of-the-art techniques including ones hand-crafted by human experts.

To automate the refactoring identification process, a large number of candidates need to be compared. Such an overhead can make the refactoring approach impractical if the software size is large and the computational load of a fitness function is substantial. In this paper, we propose a two-phase assessment approach to improving the efficiency of the process. For each iteration of the refactoring process, refactoring candidates are preliminarily assessed using a lightweight, fast delta assessment method called the Delta Table. Using multiple Delta Tables, candidates to be evaluated with a fitness function are selected. A refactoring can be selected either interactively by the developer or automatically by choosing the best refactoring, and the refactorings are applied one after another in a stepwise fashion. The Delta Table is the key concept enabling a two-phase assessment approach because of its ability to quickly calculate the varying amounts of maintainability provided by each refactoring candidate. Our approach has been evaluated for three large-scale open-source projects. The results convincingly show that the proposed approach is efficient because it saves a considerable time while still achieving the same amount of fitness improvement as the approach examining all possible candidates.

We present a new data-driven approach to achieve highly cost-effective context-sensitive points-to analysis for Java. While context-sensitivity has greater impact on the analysis precision and performance than any other precision-improving techniques, it is difficult to accurately identify the methods that would benefit the most from context-sensitivity and decide how much context-sensitivity should be used for them. Manually designing such rules is a nontrivial and laborious task that often delivers suboptimal results in practice. To overcome these challenges, we propose an automated and data-driven approach that learns to effectively apply context-sensitivity from codebases. In our approach, points-to analysis is equipped with a parameterized and heuristic rules, in disjunctive form of properties on program elements, that decide when and how much to apply context-sensitivity. We present a greedy algorithm that efficiently learns the parameter of the heuristic rules. We implemented our approach in the Doop framework and evaluated using three types of context-sensitive analyses: conventional object-sensitivity, selective hybrid object-sensitivity, and type-sensitivity. In all cases, experimental results show that our approach significantly outperforms existing techniques.

Context-awareness of mobile applications yields several issues for testing, since the mobile applications should be testable in any environment and with any contextual input.In previous studies of testing for Android applications as eventdriven systems, many researchers have focused on using the generated test cases considering only GUI events.However, it is difficult to detect failures in the changes in the context in which applications run.It is important to consider various contexts since the mobile applications adapt and use novel features and sensors of mobile devices.In this paper, we provide the method of systematically generating various executing contexts from permissions.By referring the lists of permissions, the resources that the applications use for running Android applications can be inferred easily.The various contexts of an application can be generated by permuting resource conditions, and the permutations of the contexts are prioritized.We have evaluated the usefulness and effectiveness of our method by showing that our method contributes to detect faults.

SUMMARY Automated and effective testing for function block diagram (FBD) programs has become an important issue, as FBD is increasingly used in implementing safety‐critical systems. This work describes an automated test case generation technique for FBD programs and its associated tool—FBDTester. Given an FBD program and desired test coverage criteria, FBDTester generates test requirements and invokes the Satisfiability Modulo Theories solver iteratively to derive a set of test cases. An industrial case study using reactor protection system software shows that the automatically generated test suites detected at least 82% of the known faults, whereas manually generated test cases only detected approximately 35%. Mutation analysis revealed that the automatically generated test suites substantially outperformed manually generated ones. Although test sequence generation requires some manual effort in the current FBDTester, it is apparent that the proposed approach significantly improves the efficiency and the reliability of FBD testing. Copyright © 2014 John Wiley & Sons, Ltd.

Address resolution protocol (ARP) is widely used to maintain mapping between data link (e.g. MAC) and network (e.g. IP) layer addresses. Although most hosts rely on automated and dynamic management of ARP cache entries, current implementation is well-known to be vulnerable to spoofing or denial of service (DoS) attacks. There are many tools that exploit vulnerabilities of ARP protocols, and past proposals to address the weaknesses of the ‘original’ ARP design have been unsatisfactory. Suggestions that ARP protocol definition be modified would cause serious and unacceptable compatibility problems. Other proposals require customised hardware be installed to monitor malicious ARP traffic, and many organisations cannot afford such cost. This study demonstrates that one can effectively eliminate most threats caused by the ARP vulnerabilities by installing anti-ARP spoofing agent (ASA), which intercepts unauthenticated exchange of ARP packets and blocks potentially insecure communications. The proposed approach requires neither modification of kernel ARP software nor installation of traffic monitors. Agent uses user datagram protocol (UDP) packets to enable networking among hosts in a transparent and secure manner. The authors implemented agent software on Windows XP and conducted an experiment. The results showed that ARP hacking tools could not penetrate hosts protected by ASA.

ABSTRACT Successful Security Risk Analysis (SRA) enables us to develop a secure information management system and provides valuable analysis data for future risk estimation. One of the qualitative techniques for SRA is the scenario method. This provides a framework for our explorations that raises our awareness and appreciation of uncertainty. However, the existing scenario methods are too abstract to be applicable to some situations and have not been formalized in information systems (ISs) because they do not explicitly define artifacts or have any standard notation. Therefore, this paper proposes the improved scenario‐based SRA approach, which can create SRA reports using threat scenario templates and manage security risk directly in ISs. Furthermore, in order to show how to apply the proposed method in a specific environment, especially in a Broadband convergence Network (BcN) environment, a case study is presented. Copyright © 2011 John Wiley & Sons, Ltd.

ABSTRACT Despite much research on defense against phishing attacks, incidents continue to occur where sensitive (e.g., personal or financial) information is stolen using social engineering and technical spoofing techniques. Most approaches use the notions of blacklists versus whitelists (WWLs), and it is difficult to quantify the degree of a website's vulnerability against phishing attacks. In this paper, we present a quantitative approach for evaluating the phishing possibility of a given website using the refined security risk elements for domain and web page. Design and implementation of the website risk assessment system for antiphishing are also included. It can detect suspicious websites containing phishing attack and abnormal behavior and generates a warning if website is judged untrustworthy. Copyright © 2012 John Wiley & Sons, Ltd.

This paper describes how scrum method was customized for outsourced e-commerce software projects. While the waterfall process was used in the past, outsourced projects experienced more delays and failures than the ones conducted in-house. To overcome such limitations, we decided to tailor the scrum method on three aspects: First, we produced a table that explains roles and responsibilities of project team members for every phase of the Scrum methodology. Second, we divided sprint planning into two phases, a master sprint plan and individual sprint plans. Finally, we monitored project progress based on the number of completed web pages. Application of the modified scrum method on two projects not only improved product quality but also reduced time necessary to complete the project. More than 80% of the software engineers also expressed satisfaction of the proposed approach.

Formal verification plays an important role in demonstrating the quality of safety-critical systems such as nuclear power plants. We have used the VIS verification system to determine behavioral equivalence between two successive revisions in developing the KNICS RPS (Reactor Protection System) in Korea. The VIS accepts a high-level programming language Verilog as input, and its verification results contain valuable information about one reason of the failure. However the VIS offers no graphical interface, and partially displays relevant information necessary to understand the full verification scenario accurately. Many nuclear engineers and verification experts found the information insufficient, and it makes hard to the wide use of the VIS verification system in industry. This paper proposes the VIS Analyzer, a visual assistant for VIS verification and analysis, which can help nuclear engineers take full benefits of VIS without being overwhelmed by incomplete and low-level details. The VIS Analyzer automates the VIS verification processes such as equivalence checking and model checking, and displays the verification results in visual formats. We used a recent case study introduced in to demonstrate its effectiveness and usefulness.

Abstract Accuracy of implicit path enumeration technique (IPET), which statically estimates the worst‐case execution time of a program using integer linear programming, relies on flow information captured as flow facts. Unfortunately, flow facts are inadequate for capturing complex and often subtle path constraints such as causalities. Manual annotation often introduces many disjunctions, and performance of IPET computation suffers significantly. This paper proposes a technique of encoding a subset of path constraints into flow facts. The technique has advantages over conventional approaches: (1) translation process is fully automated and (2) efficient IPET computation is possible because generated flow facts are compact in that they contain at most one disjunction. To demonstrate the effectiveness of our technique, a software tool was implemented to automatically generate flow facts for the subset of path constraints and case study has been conducted using public benchmark suites, GNU openSSH codes, and Korea multi‐purpose satellite (KOMPSAT‐1) software. Copyright © 2009 John Wiley & Sons, Ltd.

Formal verification of Function Block Diagram (FBD) based software is an essential task when replacing traditional relay-based analog system with PLC-based software in nuclear reactor protection system (RPS). FBD programs are developed manually and revised frequently in process of development. There are a set of properties to be verified formally, which all FBD releases should satisfy. Whenever FBDs are modified, there is also a need to verify behavioral equivalence of subsequently modified FBDs. This paper proposes a software verification framework for FBD software in nuclear power plants. It uses SMV model checker for verifying whether an FBD meets its required properties, and VIS verification system for checking behavioral equivalence between modified FBDs. A case study, conducted using a nuclear power plant shutdown system being developed in Korea, demonstrated that the proposed verification framework is effective and useful.

Masqueraders, despite widespread use of security products such as firewalls and intrusion detection systems, are serious threats to organizations. Although anomaly detection techniques have been considered as an effective approach to complement existing security solutions, they are not widely used in practice due to poor accuracy and relatively high degree of false alarms. In this paper, we performed an empirical study investigating the effectiveness of SVM and sequence-based kernel methods. Sequence-based kernel methods showed slightly better performance than generic RBF kernel with same frequency of false alarms. In addition, the composition of two kernel methods showed that frequency of false alarms could be further reduced.

This paper presents an iterative refinement framework for static WCET analysis based on implicit path enumeration technique (IPET). We check the feasibility of IPET solutions, convert infeasible solutions to path constraints to exclude them from the analysis, and recalculate estimates whenever new path constraints are added. This process is repeated until no more constraints are extracted or a predefined time limit is reached. Since infeasible path detection itself is an undecidable problem, we propose an approximate method that checks feasibility efficiently while preserving safeness of the results. Generated path constraints are free of disjunctions; thus, amenable to integer linear program (ILP) solvers, which are used in IPET. We demonstrated the effectiveness and efficiency by conducting an experiment, where a module of flight control software of a commercial satellite developed in Korea was used

Testing for time-related behaviors of PLC software is important and should be performed carefully. We propose a structural testing technique on function block diagram (FBD) networks including timer function blocks. In order to test FBD networks including timer function blocks, we generate templates for timer function blocks and transform a unit FBD into a flow-graph using the proposed templates. We apply existing testing techniques to the generated flowgraph and describe how the characteristics of timer function blocks are reflected in the testing process. By the proposed method, FBD networks including timer function blocks can be tested thoroughly without the intermediate code which was essential in the previous FBD testing. To demonstrate the effectiveness of the proposed method, we use a trip logic of bistable processor of digital plant protection systems which is being developed in Korea.

This paper presents a model checking-based approach to dataflow testing. We characterize dataflow oriented coverage criteria in temporal logic such that the problem of test generation is reduced to the problem of finding witnesses for a set of temporal logic formulas. The capability of model checkers to construct witnesses and counterexamples allows test generation to be fully automatic. We discuss complexity issues in minimal cost test generation and describe heuristic test generation algorithms. We illustrate our approach using CTL as temporal logic and SMV as model checker.

Integration testing of embedded software is difficult because such software tends to be large and complex; it is often structured as a set of tasks whose interaction patterns can be arbitrary and nondeterministic; it is subject to frequent changes while being tested; and testing period must be minimized since the product’s life-time is short. In order to conduct integration testing in a cost-effective manner, it is essential that requirements are captured in precise notation and that test cases are automatically generated and executed whenever possible. In this paper, we demonstrate how to generate test cases from a set of Message Sequence Charts (MSCs) by constructing a semantically equivalent global finite state machine (GFSM). Test cases are expressed as a sequence of messages to be exchanged among various system entities. When transforming complex and hierarchical MSCs to a GFSM, state explosion problem is often encountered. When constructing a GFSM, we achieved significant reduction in the number of states and transitions by generating only the feasible sequences. Such reduction was possible because embedded software we used as the case study, digital TV application software, had known and well-defined initial state. We developed a graphical toolset to edit MSCs and automatically generate test cases. Users describe the required functionalities in scenarios, and test cases are automatically generated from the GFSM according to the state and transition coverage criteria. We applied the proposed approach to specify and test a substantial portion of embedded software running on a digital TV and were able to detect an error, previously unknown to the developers, that occurred due to a subtle race condition among tasks. ∗ This work has been partially supported by the Advanced

Abstract Although numerous empirical studies have been conducted to measure the fault detection capability of software analysis methods, few studies have been conducted using programs of similar size and characteristics. Therefore, it is difficult to derive meaningful conclusions on the relative detection ability and cost‐effectiveness of various fault detection methods. In order to compare fault detection capability objectively, experiments must be conducted using the same set of programs to evaluate all methods and must involve participants who possess comparable levels of technical expertise. One such experiment was ‘Conflict1’, which compared voting, a testing method, self‐checks, code reading by stepwise refinement and data‐flow analysis methods on eight versions of a battle simulation program. Since an inspection method was not included in the comparison, the authors conducted a follow‐up experiment ‘Conflict2’, in which five of the eight versions from Conflict1 were subjected to Fagan inspection. Conflict2 examined not only the number and types of faults detected by each method, but also the cost‐effectiveness of each method, by comparing the average amount of effort expended in detecting faults. The primary findings of the Conflict2 experiment are the following. First, voting detected the largest number of faults, followed by the testing method, Fagan inspection, self‐checks, code reading and data‐flow analysis. Second, the voting, testing and inspection methods were largely complementary to each other in the types of faults detected. Third, inspection was far more cost‐effective than the testing method studied. Copyright © 2002 John Wiley & Sons, Ltd.

Abstract The importance of effective requirements analysis techniques cannot be overemphasized when developing software requiring high levels of assurance. Requirements analysis can be largely classified as either structural or functional. The former investigates whether definitions and uses of variables and functions are consistent, while the latter addresses whether requirements accurately reflect users' needs. Verification of structural properties for large and complex software requirements is often repetitive, especially if requirements are subject to frequent changes. While inspection has been successfully applied to many industrial applications, the authors found inspection to be ineffective when reviewing requirements to find errors violating structural properties. Moreover, current tools used in requirements engineering provide only limited support in automatically enforcing structural correctness of the requirements. Such experience has motivated research to automate straightforward but tedious activities. This paper demonstrates that a theorem prover, PVS (Prototype Verification System), is useful in automatically verifying structural correctness of software requirements specifications written in SCR (Software Cost Reduction)‐style. Requirements are automatically translated into a semantically equivalent PVS specification. Users need not be experts in formal methods or power users of PVS. Structural properties to be proved are expressed in PVS theorems, and the PVS proof commands are used to carry out the proof automatically. Since these properties are application independent, the same verification procedure can be applied to requirements of various software systems. Copyright © 2001 John Wiley & Sons, Ltd.

This paper presents a method for the selection of test sequences from statecharts. It is shown that a statechart can be transformed into a flow graph modelling the flow of both control and data in the statechart. The transformation enables the application of conventional control and data flow analysis techniques to test sequence selection from statecharts. The resulting set of test sequences provides the capability of determining whether an implementation establishes the desired flow of control and data expressed in statecharts. Copyright © 2000 John Wiley & Sons, Ltd.

Model checking is a formal verification technique which checks the consistency between a requirement specification and a behavior model of the system by exploring the state space of the model. We apply model checking to formal verification of concurrent object-oriented systems, using an existing model checker SPIN which has been successful in verifying parallel systems. First, we propose an Actor-based modeling language, called APromela, by extending a modeling language Promela which is a modeling language supported in SPIN. APromela supports not only all the primitives of Promela, but additional primitives needed to model concurrent object-oriented systems, such as class definition, object instantiation, message send, and synchronization. Second, we provide translation rules for mapping APromela's such modeling primitives to Promela's. By giving an example of specification, translation, and verification, we also demonstrate the applicability of our proposed approach, and discuss the limitations and further research issues.

Although object-oriented paradigm is becoming a more realistic approach to the development of large-scale software systems, the existing object-oriented notations and methodologies do not fully support the development of distributed object systems. In this paper, we integrate Meta-Object Protocol (MOP) into a de facto standard object-oriented modeling language UML together to build a software architecture for distributed object systems. We propose a high-level extension of conventional MOPs, called diMOP which helps to develop distributed object systems by realizing a reflective architecture. To incorporate diMOP with UML, we introduce two new specification languages: Class Diagram Supporting diMOP (CDSM) and Dynamically Configurable Object-oriented Statemachine (DCOS), which are proposed to replace the class diagram and the state diagram of UML. The two specification languages support the specification of dynamic configuration behaviors as well as incorporating the diMOP. This paper gives a methodology to develop efficiently distributed object systems through UML.

It is well known that requirements engineering plays a critical role in software quality. The use case approach is a requirements elicitation technique commonly used in industrial applications. Software requirements are stated as a collection of use cases, each of which is written in the user's perspective and describes a specific flow of events in the system. The use case approach offers several practical advantages in that use case requirements are relatively easy to describe, understand, and trace. Unfortunately, there are a couple of major drawbacks. Since use cases are often stated in natural languages, they lack formal syntax and semantics. Furthermore, it is difficult to analyze their global system behavior for completeness and consistency, partly because use cases describe only partial behaviors and because interactions among them are rarely represented explicitly. We propose the Constraints-based Modular Petri Nets (CMPNs) approach as an effective way to formalize the informal aspects of use cases. CMPNs, an extension of Place/Transition nets, allow the formal and incremental specification of requirements. The major contributions of the paper, in addition to the formal definitions of CMPNs, are the development of: 1) a systematic procedure to convert use cases stated in natural language to a CMPN model; and 2) a set of guidelines to find inconsistency and incompleteness in CMPNs. We demonstrate an application of our approach using use cases developed for telecommunications services.

An underlying assumption for N-version programming technique is that independently developed versions would fail in a statistically independent manner However empirical studies have demonstrated that common mode failures can occur even for independently developed versions, and that common mode failures degrade system reliability. In this paper, we demonstrate that the weakest precondition analysis is effective in determining input spaces leading to common mode failures. We applied the weakest precondition to the Launch Interceptor Programs which were used in several other experiments related to the N-version programming technique. We detected 13 out of 18 fault pairs which have been known to cause common mode failure. These faults were due to logical flaws in program design. Although the weakest precondition analysis may be labor-intensive since they are applied manually our results convincingly demonstrate that it is effective for identifying input spaces causing common mode failures and further improving the reliability of N-version software.

The SCR method models a system using a set of variables and state machines whose behaviour is described by tabular notations. This paper proposes an interleaving semantics for SCR specifications in terms of timed transition systems. The semantics is given by identifying each of the components of a timed transition system from a given SCR specification. The concurrent behaviour of a SCR specification is defined as a set of computations of the resulting timed transition system.

Robot workcell programming is an application where object oriented programming paradigms can be effectively applied to handle the issues such as concurrency and autonomy. We present an object model named Task.o, and Task object Coupling (ToC) programming technique which uses Task.o objects. This approach is designed to increase the level of reusability, expandability, modifiability, and productivity. We define the development steps of using the Task.o object model and the ToC technique and demonstrate each step.

The authors propose a safety analysis method using coloured Petri nets (CPN). Their method employs a backward approach where a hazard is assumed to have occurred and backward simulation from the hazard is performed in order to determine if and how the hazard might occur. Using CPN, they define a hazard as a set of markings and perform backward simulation by generating a reachability graph backwards from the hazard. To facilitate the safety analysis, they extend the semantics of CPN and define backward reachability graphs of CPN. To demonstrate their method, a shutdown system for a Korean nuclear power plant is used as an example.

In object-oriented testing literature, a class is considered to be a basic unit of testing. A major characteristic of classes is the interaction between data members and member functions. This interaction is represented as definitions and uses of data members in member functions and can be properly modeled with finite state machines (FSM). We discuss how FSMs can be effectively used for class testing. We demonstrate how to specify the behavior of classes using FSMs and present a test case generation technique based on FSMs. In our technique, FSMs are transformed into a flow of the graph from which we can explicitly identify data flows of the FSM. Then we generate test cases using conventional data flow testing techniques upon the flow graph.

The paper presents the results of an experiment that compared error detection capability of voting, instrumentation, and Fagan inspection methods. Several experiments have measured effectiveness of various error detection methods. However, most experiments have used different programs; consequently, the results are generally incompatible and do not allow one to make objective comparison on the cost-effectiveness of various approaches. Software cannot be developed using an unlimited amount of resources, and practitioners need empirical and objective data on the cost-effectiveness of various error detection methods to decide which methods to use during software development. Results of this experiment is significant because these methods have been applied to the same program. Furthermore, the participant's educational and industrial experience are comparable to that of the previous experiments. We confirmed the previous finding that detecting errors in reliable programs is difficult; none of the three methods detected more than half of all the known errors in the programs. Of the three methods employed, participants detected more errors by using Fagan inspection method than they did by voting or instrumentation. When the average number of hours needed to detect an error was compared, Fagan inspection method was shown to be more cost-effective than instrumentation method.