To automatically test web applications, crawling-based techniques are usually adopted to mine the behavior models, explore the state spaces or detect the violated invariants of the applications. However, their broad use is limited by the required manual configurations for input value selection, GUI state comparison and clickable detection. In existing crawlers, the configurations are usually string-matching based rules looking for tags or attributes of DOM elements, and often application-specific. Moreover, in input topic identification, it can be difficult to determine which rule suggests a better match when several rules match an input field to more than one topic. This paper presents a natural-language approach based on semantic similarity to address the above issues. The proposed approach represents DOM elements as vectors in a vector space formed by the words used in the elements. The topics of encountered input fields during crawling can then be inferred by their similarities with ones in a labeled corpus. Semantic similarity can also be applied to suggest if a GUI state is newly discovered and a DOM element is clickable under an unsupervised learning paradigm. We evaluated the proposed approach in input topic identification with 100 real-world forms and GUI state comparison with real data from industry. Our evaluation shows that the proposed approach has comparable or better performance to the conventional techniques. Experiments in input topic identification also show that the accuracy of the rule-based approach can be improved by up to 22% when integrated with our approach.

The state-of-the-art model-checkers for probabilistic timed automata (PTAs) use separate representations for the dense-time and discrete parts of PTA states. In the literature, integrated state-space representations based on decision diagrams, e.g., RED diagrams (the underlying symbolic representation in the model checker RED), have shown considerable performance enhancement in model-checking timed automata (TAs) and linear hybrid automata (LHAs). A RED diagram for a TA can represent the dense-time and discrete parts of TA states in a single and integrated decision diagram. In this work, we experiment to investigate whether such performance enhancement can be duplicated with PTA model-checking. Specifically, we propose a lightweight extension to RED diagrams to represent quantitative states of PTAs in an integrated manner, yet preserving the structure-sharing capacity of RED diagrams. We then develop and implement a symbolic reachability analysis algorithm for PTAs based on the extended RED diagrams. We further carry out experiments with the PTA benchmarks from a popular probabilistic model checker PRISM to evaluate the performance of such integrated decision diagrams and the reachability analysis algorithm. Experimental results show that our approach can indeed help to improve the time-efficiency and scalability of PTA model-checking.

We introduce a novel technique for verification and model synthesis of sequential programs. Our technique is based on learning an approximate regular model of the set of feasible paths in a program, and testing whether this model contains an incorrect behavior. Exact learning algorithms require checking equivalence between the model and the program, which is a difficult problem, in general undecidable. Our learning procedure is therefore based on the framework of probably approximately correct (PAC) learning, which uses sampling instead, and provides correctness guarantees expressed using the terms error probability and confidence. Besides the verification result, our procedure also outputs the model with the said correctness guarantees. Obtained preliminary experiments show encouraging results, in some cases even outperforming mature software verifiers.

Safety-critical systems need to maintain their functionality in the presence of multiple errors caused by component failures or disastrous environment events. We propose a game-theoretic foundation for synthesizing control strategies that maximize the resilience of a software system in defense against a realistic error model. The new control objective of such a game is called $k$ -resilience. In order to be $k$ -resilient, a system needs to rapidly recover from infinitely many waves of a small number of up to $k$ close errors provided that the blocks of up to $k$ errors are separated by short time intervals, which can be used by the system to recover. We first argue why we believe this to be the right level of abstraction for safety critical systems when local faults are few and far between. We then show how the analysis of $k$ -resilience problems can be formulated as a model-checking problem of a mild extension to the alternating-time $\mu$ -calculus (AMC). The witness for $k$ resilience, which can be provided by the model checker, can be used for providing control strategies that are optimal with respect to resilience. We show that the computational complexity of constructing such optimal control strategies is low and demonstrate the feasibility of our approach through an implementation and experimental results.

We propose an extension to ATL ( alternating-time temporal logic ), called BSIL ( basic strategy-interaction logic ), for specifying collaboration among agents in a multiagent system. We show that BSIL is strictly more expressive than ATL + but incomparable with ATL * , GL ( game logic ), and AMC ( alternating μ-calculus ) in expressiveness. We show that a memoryful strategy is necessary for fulfilling a specification in BSIL. We establish that the BSIL model-checking problem is PSPACE-complete. However, BSIL model checking can be performed in time quadratic in the model for fixed formulas. The BSIL (and hence ATL + ) satisfiability is 2EXPTIME-complete. Finally, we report our experiment with a model checker for BSIL.

We present a symbolic approach for checking consistency of OpenMP parallel programs. A parallel program is consistent if it yields the same result as its sequential version despite the execution order among threads. We find race conditions of an OpenMP parallel program, construct the formal model of its raced segments under relaxed memory models, and perform guided symbolic simulation to search consistency violations. The simulation terminates when (1) a witness has been found (the program is inconsistent), or (2) all reachable states have been explored (the program is consistent). We have developed the tool Pathg by incorporating Omega library to solve race constraints and Red symbolic simulator to perform guided search. We show that Pathg can prove consistency of programs, identify races that modern OpenMP checkers failed to report, and find inconsistency witnesses effectively against benchmarks from the OpenMP Source Code Repository and the NAS Parallel benchmark suite.

A test oracle is a mechanism that decides whether an SUT (software under test) fails or passes a test case. We investigate how to use machine learning techniques to automatically construct test oracles for reactive programs without reliance on explicit specifications. Firstly, we present a library, called In TOL (Intelligent Test Oracle Library), for the convenient and flexible collection of test traces. We can flexibly use either user guidance or program assertions to collect verdicts to test traces. Such verdicts are used as supervisory signals to the supervised learning algorithm (SLA) for a test oracle. Secondly, we present several sets of feature variables for the temporal relation among events in test traces of unbounded lengths. Then we present procedures that convert test traces into feature vectors, train an SLA with the feature vectors and their verdicts, and use the trained SLA as a test oracle. We report the implementation of In TOL on top of SVM (support vector machine). We experiment with two open-source benchmark SUTs from the internet to check the performance of our techniques. Our experiment data shows that high-accuracy test verdicts can be achieved with our test oracles for the benchmark SUTs.

Word-level predicates involve high-level descriptions of integer variables and can be complex to represent and manipulate with traditional decision diagrams like BDDs (binary decision diagrams) and MDDs (multiple-valued decision diagrams). We propose a new type of decision diagram nodes, called LD-nodes (lazy decision nodes), for word-level inequalities that allow for lazy evaluation. Such nodes can be incorporated in BDDs, MDDs, and CRDs (clock-restriction diagrams). We present algorithms for operations on diagrams with LDD nodes. We then report our experiment of our technology with several benchmarks. A library implementing the approach is available at Source Forge web page for project REDLIB.

The evaluation of successor or predecessor state spaces through time progress is a central component in the model-checking algorithms of dense-time automata. The time progress operator takes the concavity of a path condition into consideration and usually results in high complexity in the evaluation. Previous algorithms in this aspect usually assume that the location invariance condition of an automaton are convex in the dense-time state space and use a more efficient algorithm for time progress evaluation. In fact, the restriction of location invariance condition convexity can be further relaxed to that of time-convexity for a broader range of application of the more efficient algorithm. In this work, we present techniques for the efficient model-checking of dense-time automata by taking the time-convexity of path conditions into consideration. We first identify a class of TCTL formulas that only characterize time-convex state spaces. The class includes several important types of TCTL formulas, including some timed inevitabilities with deadlines. We then present a new formulation for the efficient evaluation of timed inevitabilities with time-convex path conditions. The new formulation also leads to a new technique for the approximate evaluation of timed inevitabilities with better precision. Finally, we report our implementation and experiment.

In this work, we discuss testing automation issues for kernel code on a high-capacity network-attached storage (NAS) in early development phases when the hardware may not be ready. We propose to construct a high-fidelity versatile emulator for hard disks for the fast configuration of virtual disk arrays. To test kernel libraries, we not only have to figure out the proper values for the kernel procedure parameters, but also have to overcome the rigid resource limitations in kernel space. We propose techniques to profile kernel procedure parameters, drive the kernel procedures from the user space, and construct the testing interface between kernel SUTs (software-under-test) and user space test plans. We have experimented to test the multiple devices driver library used in the NAS server by Quanta Computer Inc. Our techniques support rapid NAS configurations and have been proven useful in locating a proven bug in the Linux kernel

To promote the technology of dense-time system model-checking in both academia and industry, we developed a library, called REDLIB, which supports full TCTL model- checking of dense-time automata with multiple fairness assumptions. REDLIB uses the BDD-like diagrams for the efficient representation and manipulation of dense-time state- spaces. Users can use the procedures in REDLIB to quickly construct dense-time models and carry out basic Boolean and state-space operations, postcondtion/precondition calculation, state-space representation normalizations, greatest fixpoint calculation, parametric safety analysis of linear hybrid systems, speed-up techniques for greatest fix- point evaluation, and coverage analysis of dense-time state- spaces. REDLIB also has a preprocessor that allows for high-level constructs like arrays, message channels, dynamic memory allocation, procedure calls, and timers. In this article, we discuss the features of REDLIB and give small examples to show how to use REDLIB.

Inevitability properties in branching temporal logics are of the syntax foralldiamphi, where phi is an arbitrary (timed) CTL (computation tree logic) formula. Such inevitability properties in dense-time logics can be analyzed with the greatest fixpoint calculation. We present algorithms to model-check inevitability properties. We discuss a technique for early decision on greatest fixpoint calculation which has shown promising performance against several benchmarks. We have experimented with various issues which may affect the performance of TCTL inevitability analysis. Specifically, our algorithms come with a parameter for the measurement of time-progress. We report the performance of our implementation with regard to various parameter values and with or without the non-Zeno computation requirement in the evaluation of greatest fixpoints. We have also experimented with safe abstraction techniques for model-checking TCTL inevitability properties. The experiment results help us in deducing rules for setting the parameter for verification performance. Finally, we summarize suggestions for configurations of efficient TCTL inevitability evaluation procedure

We introduce a new BDD-like data structure called hybrid-restriction diagrams (HRDs) for the representation and manipulation of linear hybrid automata (LHA) state-spaces and present algorithms for weakest precondition calculations. This permits us to reason about the valuations of parameters that make safety properties satisfied. Advantages of our approach include the ability to represent discrete state information and concave polyhedra in a unified scheme, as well as to save both memory consumptions and manipulation times when processing the same substructures in state-space representations. Our experimental results document its efficiency in practice.

An overview of the current state of the art of formal verification of real-time systems is presented. We discuss commonly accepted models, specification languages, verification frameworks, state-space representation schemes, state-space construction procedures, reduction techniques, pioneering tools, and finally some new related issues. We also make a few comments according to our experience with verification tool design and implementation.

Dynamic data-structures with pointer links, which are heavily used in real-world software, cause extremely difficult verification problems. Currently, there is no practical framework for the efficient verification of such software systems. We investigated symmetry reduction techniques for the verification of software systems with C-like indirect reference chains like x/spl rarr/y/spl rarr/z/spl rarr/w. We formally defined the model of software with pointer data structures and developed symbolic algorithms to manipulate conditions and assignments with indirect reference chains using BDD technology. We relied on two techniques, inactive variable elimination and process-symmetry reduction in the data-structure configuration, to reduce time and memory complexity. We used binary permutation for efficiency, but we also identified the possibility of an anomaly of false image reachability. We implemented the techniques in tool Red 5.0 and compared performance with Mur/spl phi/ and SMC against several benchmarks.

A compositional verification method from a high-level resource-management standpoint is presented for dense-time concurrent systems and implemented in the tool of SGM (State-Graph Manipulators) with graphical user interface. SGM packages sophisticated verification technology into state-graph manipulators and provides a user interface which views state-graphs as basic data-objects. Hence, users do not have to be verification theory experts and do not have to trace inside state-graphs to analyze state and path properties to make the best use of verification theory. Instead, users can construct their own verification strategies based on observation on the state-graph complexity changes after experimenting with some combinations of manipulators. Moreover, SGM allows users to control the complexity of state-graphs through iterative state-graphs merging and reductions before they become out of control, Reduction techniques specially designed for the context of state-graph iteration composition and shared variable manipulations are developed and used in SGM. Experiments on different benchmarks to show SGM performance are reported. An algorithm based on group theory to pick a manipulator combination is presented.

RED (Region Encoding Diagram), first reported by F.Wang (2000), is a BDD-like data structure for fully symbolic verification of symmetric real time systems with single clock per process. We propose to extend RED for asymmetric real time systems with an unrestricted number of global or local clocks. Unlike in DBM which records differences between pairs of clock readings, we record the ordering among fractional parts of clock readings into integer sequences encoded in RED's. Like BDD, the new RED is also a minimal canonical form for its target system state-space representations. The number of variables used in RED is O(|X|log|X|) where X is the clock set in the input system description. Experimentation has been carried out to compare RED's performance with the tools: UPPAAL2K and Kronos. Accordingly, we found out that RED is the most efficient real time system safety analyzer as long as concurrency complexity is considered.

In this article, we consider symbolic model checking for event-driven real-time systems.We first propose a Synchronous Real-Time Event Logic (SREL) for capturing the formal semantics of synchronous, event-driven real-time systems.The concrete syntax of these systems is given in terms of a graphical programming language called Modechart, by Jahanian and Mok, which can be translated into SREL structures.We then present a symbolic model-checking algorithm for SREL.In particular, we give an efficient algorithm for constructing OBDDs (Ordered Binary Decision Diagrams) for linear constraints among integer variables.This is very important in a BDD-based symbolic model checker for real-time systems, since timing and event occurrence constraints are used very often in the specification of these systems.We have incorporated our construction algorithm into the SMV v2.3 from Carnegie-Mellon University and have been able to achieve one to two orders of magnitude in speedup and space saving when compared to the implementation of timing and event-counting functions by integer arithmetics provided by SMV.

We extend TCTL model-checking problem to timing behavior analysis problem for real-time systems and develop new techniques in solving it. The algorithm we present here accepts timed transition system descriptions and parametric TCTL formulas with timing parameter variables of unknown sizes and can give back general linear equations of timing parameter variables whose solutions make the systems working.

We consider symbolic model-checking for event-driven real-time systems. The concrete syntax of these systems is given in terms of a graphical programming language called Modechart. We propose a logic, Synchronous Real-Time Event logic (SREL) for specifying the timing properties of these systems. We then present a symbolic model-checking algorithm which checks a modechart against an SREL formula, and discuss several implementation issues. In particular, we give an efficient solution to the problem of encoding timing and event counting functions based on Binary Decision Diagram (BDD). This solution has been incorported into the SMV system v2.3 and has been able to achieve one to two orders of magnitude in speedup and space saving when compared to the solution based on the integer operations provided by the SMV system.>

In this article, we propose a language, Asynchronous Propositional Temporal Logic (APTL), for the specification and verification of distributed hard real-time sytems. APTL extends the logic TPTL by dealing explicitly with multiple local clocks. We propose a distributed-system model which permits definition of inequalities asserting the temporal precedence of local clock readings. We show the expressiveness of APTL through two nontrivial examples. Our logic can be used to specify and reason about such important properties as bounded clock rate drifting. We then give a 2 2 0(n) tableau-based decision procedure for determining APTL satisfiability, where n is the size (number of bits) of the input formula.

Article Free Access Share on Formal specification of asynchronous distributed real-time systems by APTL Authors: Farn Wang View Profile , Al Mok View Profile , E. Allen Emerson View Profile Authors Info & Claims ICSE '92: Proceedings of the 14th international conference on Software engineeringJune 1992 Pages 188–198https://doi.org/10.1145/143062.143113Published:01 June 1992Publication History 4citation137DownloadsMetricsTotal Citations4Total Downloads137Last 12 Months5Last 6 weeks0 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF