With traditional testing, the test case has no control over non-deterministic scheduling decisions, and thus errors dependent on are only found by pure chance. Java Path Finder (JPF) is a specialized virtual machine that can systematically explore execution paths for all possible schedulings, catch these errors. Unfortunately, execution-based model checkers, including JPF, cannot be easily adapted to support real-time programs.

Although there exist several software model checkers that check the code against properties specified e.g. via a temporal logic and assertions, or just verifying low-level (like unhandled exceptions), none of them supports checking components high-level behavior specification. We present our approach to implemented in Java specification their defined protocols, which employs PathFinder checker protocol checker. The property checked by (JPF) tool (correctness particular method call sequences)...

Java Pathfinder (JPF) was originally developed as an explicit state software model checker and subsequently evolved into extensible bytecode analysis framework that has been successfully used to implement techniques such symbolic concolic execution, compositional verification, parallel incremental program analysis, many more. Apart from its original domain of concurrent programs, JPF now supports the verification new domains UMLs, numeric graphical user interfaces, Android applications.

Model checking of isolated software components is inherently not possible because a component does form complete program with an explicit starting point. To overcome this obstacle, it typically necessary to create environment the which intended subject model checking. We present our approach automated generation that based on behavior protocols [Plasil, F., and S. Visnovsky, Behavior Protocols for Software Components, IEEE Transactions Engineering, 28(2002)]; knowledge, only generator...

Application of model checking to isolated software components is not directly possible because a component does form complete program - the problem missing environment occurs. A solution create an some for subject checking. As most general can cause be infeasible, we on basis particular context used in. More specifically, our approach exploits hierarchical architecture and behavior specification defined via protocols, all that provided in ADL. This way, represents rest application with...

One popular approach to detect errors in multi-threaded programs is systematically explore all possible interleavings. A common algorithmic strategy construct the program state space on-the-fly and perform thread scheduling choices at any instruction that could have effects visible other threads. Existing tools do not look ahead code be executed, thus their decisions are too conservative. They create unnecessary instructions actually influence threads, which implies exploring exponentially...

Our goal is to develop precise and scalable verification techniques for Java programs that use collections properties depend on their content. We apply the popular approach of predicate abstraction collections. The main challenge in this context compact modeling enables practical verification. define a language observable state at interface level. Changes by API methods are captured weakest preconditions. adapt existing construction abstract programs. Most notably, we designed optimizations...

Real-time systems, and in particular safety-critical are a rich source of challenges for the program verification community as software errors can have catastrophic consequences. Unfortunately, it is nearly impossible to find representative programs public domain. This has been significant impediment research field, very difficult validate new ideas or techniques experimentally. paper presents open real-time systems context Specification Java. But, our main contribution family programs,...

Code model checking of software components suffers from the well-known problem state explosion when applied to highly parallel components, despite fact that a single component typically comprises smaller space than whole system. We present technique mitigates in code primitive with Java PathFinder case checked property is absence concurrency errors. The key idea reduce parallelism calling protocol on basis information provided by static analysis searching for concurrency-related patterns...

A key problem in compositional model checking of software systems is that typical checkers accept only closed (runnable programs) and therefore a component cannot be model-checked directly. solution to create an artificial environment for the such its composition forms runnable program can model-checked. Although it possible universal performs all sequences interleavings calls component's methods, practical purposes sufficient capture this way just use particular system – idea expressed by...

We present our ongoing effort to implement predicate abstraction in Abstract Pathfinder, which is an extension of Java Pathfinder. Our approach builds upon existing techniques that have been proposed mainly for low-level programs C. support predicates over variables having numerical data types. The main challenges we addressed include (1) the design language, (2) arrays, (3) finding affected by a given statement, (4) aliasing between variables, (5) propagating values method call boundaries,...

Techniques and tools for verification of multi-threaded programs must cope with the huge number possible thread interleavings. Tools based on systematic exploration a program state space employ partial order reduction to avoid redundant The key idea is make non-deterministic scheduling choices only at statements that read or modify global shared by multiple threads. We focus approach used in such as Java Pathfinder (JPF), which construct on-the-fly, therefore can use information available...

Although Web services are generally envisioned as being stateless, some of them implicitly stateful. The reason is that the often work front-ends to enterprise systems and used in a session-oriented way by clients. Contrary case stateless services, for stateful service there exist constraints order which operations may be invoked. However, specification such not standard part interface, compliance with checked development tools. Therefore, we propose this paper extend web interface...

We present Abstract Pathfinder, an extension to the Java Pathfinder (JPF) verification tool-set that supports data abstraction reduce large domains of a program small, finite abstract domains, making more amenable verification. use compute over-approximation original in such way if (safety) property is true abstracted also program. Our approach enhances JPF with interpreter and state-matching mechanisms, together library abstractions from which user can pick for particular application....

Our goal is to develop precise and scalable verification techniques for Java programs that use collections properties depend on their content. We apply the popular approach of predicate abstraction collections. The main challenge in this context compact modeling enables practical verification. define a language observable state at interface level. Changes by API methods are captured weakest preconditions. adapt existing construction abstract programs. Most notably, we designed optimizations...

In software component verification, one of the challenges is model checking isolated components. The environment an unknown, and therefore a part input to checker missing. This problem can be addressed via automated generation artificial — its form complete program that verified using common checkers. Focusing on concurrency errors in Java components, we propose automatically generate reasonable makes efficient detection with PathFinder possible. Such executes parallel those component's...

Fostering efficiency of distributed supply chains in the Industry 4.0 often bases on IoT-data analysis and by means lean- shop oor-management. However, trust preserving privacy is a precondition: Competing factories will not share data, if, e.g., data reveal business relevant information to competitors. Our approach enforcing policies chains. These are highly dynamic therefore manageable 'traditional' rights-management approaches as we stretch literature analysis. To enforce privacy, analyze...

A popular approach to verification of software system correctness is model checking. To achieve scalability needed for large systems, checking has be augmented with abstraction. In this paper, we provide an overview selected techniques program based on predicate We focus that advanced the state-of-the-art in a significant way, including counterexample-guided abstraction refinement, lazy abstraction, and current trends form extensions targeting, example, data structures multi-threading....