In recent years, data spaces have emerged as a framework for secure data collaboration. Data spaces are distributed data collaboration infrastructure systems that enable data collaboration among stakeholders. One of the requirements for data space systems is the technical enforcement of governance policies for the shared data. The objective of this study is to propose a new policy definition language, DSPOL, as a stepping stone toward realizing the enforcement of data governance for the practical use of data spaces. DSPOL can describe the constraints that must be followed in data space systems when accessing and using data, and when distributing deliverables. It has verification and validation functions to ensure that the policy description is as the writer intended and that there are no inconsistencies in the policy. We defined the state transitions of data usage in data user environments, developed a model of the execution infrastructure in data space systems, and formulated the contents of the describable policies. We implemented DSPOL and its verification and validation functions. Examples of policy descriptions based on supposed scenarios were shown, and examples of verification and validation were presented.

Testing a program to confirm whether it consistently implements its requirements specification is a necessary but time-consuming activity in software development. Automatic testing based on specifications can significantly alleviate the workload and cost, but faces a challenge of how to ensure that both the user’s concerns in the specification and possible execution paths in the program are all covered. In this paper, we describe a new method, called “Vibration-Method” or simply “V-Method”, for automatic generation of test cases and test oracle from model-based formal specifications, aiming to address this challenge. The proposed method is suitable for testing information systems in which rich data types are used. Supporting the principle of “divide and conquer”, the method provides a specific technique for generating test cases based on functional scenarios defined in the specification, test case generation criteria, automatic test case generation algorithms, and a well-defined mechanism for deriving test oracle. We elaborate on the method by discussing how initial test cases can be automatically generated, how additional necessary test cases are produced using the “vibration” technique, and how a test oracle can be automatically derived for a group of test cases. We also describe a controlled experiment to evaluate the effectiveness of the method and discuss the important issues in relation to the performance and applicability of the method.

In a world where many human lives depend on the correct behavior of software systems, program verification assumes a crucial role. Many verification tools rely on an algorithm that generates verification conditions (VCs) from code annotated with properties to be checked. In this paper, we revisit two major methods that are widely used to produce VCs: predicate transformers (used mostly by deductive verification tools) and the conditional normal form transformation (used in bounded model checking of software). We identify three different aspects in which the methods differ (logical encoding of control flow, use of contexts, and semantics of asserts), and show that, since they are orthogonal, they can be freely combined. This results in six new hybrid verification condition generators (VCGens), which together with the fundamental methods constitute what we call the VCGen cube. We consider two optimizations implemented in major program verification tools and show that each of them can in fact be applied to an entire face of the cube, resulting in optimized versions of the six hybrid VCGens. Finally, we compare all VCGens empirically using a number of benchmarks. Although the results do not indicate absolute superiority of any given method, they do allow us to identify interesting patterns.

IoT devices are software-rich and Java is sometimes chosen as the developing programming language. Although Java is highly productive in constructing large advanced programs, application or user-defined Java classes must be responsible for safety and security issues. In particular, two fundamental methods hashCode and equals play key roles in safety and security assurance. Some existing studies for ensuring the correctness of these two methods rely on static analysis, which are limited to loop-free programs only. This paper proposes a new solution to this important problem, based on equivalence checking of methods or functions. The proposed approach makes use of software analysis workbench (SAW), an open source tool. The approach is also useful in reducing the cost of regression testing when program refactoring is conducted.

Machine learning programs are non-testable, and thus testing with pseudo oracles is recommended. Although metamorphic testing is effective for testing with pseudo oracles, identifying metamorphic properties has been mostly ad hoc. This paper proposes a systematic method to derive a set of metamorphic properties for machine learning classifiers, support vector machines. The proposal includes a new notion of test coverage for the machine learning programs; this test coverage provides a clear guideline for conducting a series of metamorphic testing.

In formula-based fault localization methods, a program under test, which is unrolled to a certain bound, is encoded in a trace formula (TF). The efficiency and precision of the fault localization algorithm depend highly on the way this formula is encoded. The full flow-sensitive TF can cover all potential root causes, but is usually large and scalability problems remain. We propose a new encoding, the hardened flow-sensitive trace formula (HFTF), which reduces the complexity of the formula but does not lose essential control flow graph (CFG) information required for localizing faults. The HFTF is constructed using a concolic execution method that generates both failing and successful executions and uses the coverage information from these executions to simplify the trace formula.

Open systems such as Web applications are dynamically adaptive to allow desired levels of flexibility. The adaptibity may be achieved by replacing constituent software components at runtime, and a new method is required to ensure that the replacement or substitution is safe. This paper proposes a formal framework of safe substitution for self-adaptive systems and presents a policy-based, system integrity verification method. In an example case, an adaptive Web application demonstrates the effectiveness of the proposed approach.

Behavior of open systems is subject to dynamically changing external environment. Runtime monitoring and checking methods are employed to detect interference of functional features in these open systems. Such checking usually has a large impact on the runtime performance. The overhead of checking is unavoidable for fatal anomalies. For less severe anomalies, the performance penalty is not acceptable if the occurrence rate is very small. This paper proposes a new method of estimating the occurrence rate of rare events at runtime with the importance sampling. It is the first report of applying the method to running systems, instead of using discrete simulation models or design models.

Model-Based Development (MBD) is a promising approach to achieving the required reliability levels of Cyber-Physical Systems. These systems are inherently heterogeneous. For example, models such as a controller and a plant have different characteristics. This paper proposes a Co-Analysis method. Logic-based analysis is employed to deal with an under-constrained or non-deterministic controller described with SysML. The analysis of the plant with Simulink adapts numerical simulation methods since the model represents physical phenomena whose time-dependent behavior is deterministic but computed with the initial states. The paper discusses further issues with the proposed co-analysis method.

Several approaches to test case generation based on formal specifications have been put forward, but how to automatically generate test cases to ensure that all of the representative program paths of the corresponding program are traversed still remains an open problem. In this paper, we describe a new technique called "Vibration" method to tackle this problem. The method focuses on a heuristic process of generating test cases, collecting traversed paths, and removing the bugs detected, based on a single test condition of a functional scenario until all the corresponding program paths are traversed or a stopping testing condition is met. The test case generation is fully automatic, in the sense that all the criteria can be implemented by algorithms in a software tool. We describe the criteria and algorithms for test case generation and for stopping a testing process.

Self-adaptive systems, changing their functional behavior at runtime, provide desired a level of flexibility. Although various runtime frameworks have been studied, they tend to rely on a particular architecture. It is inadequate to study the characteristics of self-adaptive systems. This paper presents an abstract, declarative framework for them and relates it to an adaptive PHP-based Web application architecture, which takes a model-based adaptation approach. The formalism can be a basis for understanding the distinctive roles of the model information and runtime mechanism.

To verify behavioral specification of compound Web services, this paper introduces to apply model checking to Web services flows described by BPEL. Model checking is a formal method to formalize the behavior of designed system as an automaton and to analyze automatically whether or not the automaton satisfies the specification. This paper introduces translation pattern to convert a BPEL process to Promela code (Process or Protocol Meta Language), which is a verification modeling language in SPIN model checker. The result of our case study using a parking navigation service shows that our translation pattern can automatically verify the specification except Exception handling pattern and Event handling pattern.

Software risk comes mainly from its poor reliability, but how to effectively achieve high reliability still remains a challenge. This paper puts forward a framework for systematically integrating formal specification, review, and testing, and shows how it can be applied to effectively eliminate errors in the major phases of software development process to enhance software reliability. In this framework, requirements errors can be removed and missing requirements can be identified by formalizing requirements into formal specifications whose validity can be ensured by rigorous review. The valid specification can then be used as a firm foundation for implementation and for rigorous inspection, testing, and walkthrough of the implemented program. We discuss how formalization, review, and testing work together at different levels of software development to improve software reliability through detecting and removing errors in documentation.

A new algorithm for generating counterexamples for the temporal description logic ALCCTL is presented. ALCCTL is a decidable combination of the description logic ALC and computation tree logic CTL. It extends CTL by first order quantified expressions over unary and binary predicates. Predicates and quantified expressions are required for representing properties in application domains such as structured web documents and they are frequently used in software and hardware specifications which are verified by model checking. In the case of a specification violation, existing algorithms generate counterexamples that tend to be complex yet imprecise if specifications range over sets of objects. The presented algorithm is the first algorithm for generating counterexamples for a temporal description logic that considers first order predicates and quantification. The algorithm is sound and semi-complete for ALCCTL. The generated counterexamples are both more precise and comprehensible than counterexamples generated by the previous algorithms.

Functional scenario-based test case generation is an important technique for specification-based testing and it can be fully automated. The vital first step of achieving the automation is automatic transformation from a formal specification into an equivalent functional scenario form from which all functional scenarios are derived. In this paper, we first explain the concepts of the functional scenario form and the functional scenario in the context of a VDM operation specification, and then discuss the techniques for the transformation implemented in a software tool we have built. The techniques for discussion include (1) transformation from compound expressions into predicate expressions, (2) transformation from quantified expressions into non-quantified expressions, (3) replacing implications and equivalences in predicate expressions, (4) transformation from predicate expressions into functional scenario forms, and (5) the derivation of the testing condition from a functional scenario for test case generation. Based on these transformations, the tool can also automatically produce test cases to meet required conditions.

Static program analysis is promising as a complement to conventional testing methods relying on program executions. This paper introduces VARVEL, a SAT-based bounded model-checker for C programs. It has a notion of Design by Contract (DbC) explicitly and therefore modular checking of large C programs is achieved to resolve the scalability problem that model-checkers are usually faced with. Further, VARVEL provides advanced DbC features in that we can handle C programs having pointers to functions, re-entrancy problems, and defensive programming style. We also report some results of using VARVEL for the analysis of industrial C programs.

Aspect-oriented programming (AOP) is a technique for modularizing crosscutting concerns (CCCs). A variety of CCCs can be found in typical Web applications. Most CCCs are scattered over Web-specific events such as page requests. AOWP, a PHP-based AOP framework, provides Web-specific aspect instantiations for dealing with session management and pointcut & advice mechanisms for capturing Web-specific events. CCCs in Web applications can be clearly modularized by introducing AOWP.

We propose a new domain-specific aspect-oriented programming (AOP) mechanism for Web application development. A variety of crosscutting concerns such as access control and performance tuning are found in typical Web applications, but it is not easy to concisely modularize the concerns as aspects in current AOP languages because they do not provide pointcut mechanisms for directly handling events in the Web controller layer. To deal with this problem, we propose a Web-specific AOP mechanism called AOWP and a PHP-based AOWP framework. Using this framework, a programmer can easily address Web-specific crosscutting concerns triggered by Web-specific events, including page requests, page transitions, and session management events.

Model-checking is a promising technique for the verification and validation of systems. Practical systems need complicated design descriptions because they often refer to situations concerning exceptional cases in addition to normal, regular behaviour. Since properties deal with many exceptional cases, the property formulae to be verified become complicated and hard to understand. Further, as both system and property descriptions are complicated, the state space searched in the model-checking process becomes large, which affects execution performance. This paper employs a model-checking technique based on multivalued transition systems to reduce such complexities. It discusses advantages by applying the idea to an example case of the behavioural analysis of the EJB component framework.

Web service is an emerging software technology to use remote services in the Internet. As it becomes pervasive, some "language" to describe Web service flows is needed to combine existing services flexibly. The flow essentially describes distributed collaborations and is not easy to write and verify, while the fault that the flow description may contain can only be detected at runtime. The faulty flow description is not desirable because a tremendous amount of publicly shared network resources are consumed. The verification of the Web service flow prior to its execution in the Internet is mandatory. This paper proposes to use the software model-checking technology for the verification of the Web service flow descriptions. For a concrete discussion, the paper adapts WSFL (Web Services Flow Language) as the language to describe the Web service flows, and uses the SPIN model-checker for the verification engine. The experiment shows that the software model-checking technology is usable as a basis for the verification of WSFL descriptions.

This paper reports a directory server in a distributed middleware for realizing the interoperability between a wide variety of mobile agent systems. The ODP trader, an ITU-T recommendation for direction service, is customized for the specific requirements. The key ideas are (1) to extend the managed information so that program codes can be members, and (2) to provide Proxy Offer for utilizing services located outside the directory. Performance measurement shows that Proxy Offer is more efficient than dynamic property of the ODP trader in the current application.

We have developed a light-weight Q3 agent platform that is embedded in subscriber network elements. We have reexamined requirements in OSI recommendations, and then we have omitted functionalities redundant for subscriber network elements. As a result, the platform can use effective architectures, such as main-memory MIB, for a high performance and cost effective agent. We have especially made efforts at designing efficient data structures of class information and attributes. An agent application built on the platform achieves 400 M-GET operations per second and 150 event reports per second.

A scenario-based object-oriented modeling method for algebraic specifications is proposed.The method is based on the integration of a new algebraic specification language, CafeOBJ, and a multiparadigm design notation, GIL0-2 (Generic Interaction Language for Objects).CafeOBJ is a successor of the algebraic specification language OBJ and supports object-oriented formal specifications based on hidden order sorted rewriting logic.GIL0-2 provides collaborations as well as classes of objects to capture behavioral aspects of scenarios in object-oriented modeling.Given a problem description of the system to develop, the proposed method provides guidelines for decomposing the problem into executable CafeOBJ specification modules through scenario-based object-oriented design in GIL0-2; the decomposition reflects the structure of the problem domain.The proposal also indicates how formal executable specification in CafeOBJ can be systematically obtained from the design in GIL0-2.