Recently, a lot of low-light image enhancement methods have been proposed. However, these methods have some problems such as causing fine details lost in bright regions and/or unnatural color tones. In this paper, we propose a new low-light image enhancement method to cope with these problems. In the proposed method, a pixel is represented by a convex combination of white, black, and pure color. Then, an equi-hue plane in RGB color space is represented as a triangle whose vertices correspond to white, black, and pure color. The visibility of low-light image is improved by applying a modified gamma transform to the combination coefficients on an equi-hue plane in RGB color space. The contrast of the image is enhanced by the histogram specification method using the histogram smoothed by a filter with a kernel determined based on a gamma distribution. In the experiments, the effectiveness of the proposed method is verified by the comparison with the state-of-the-art low-light image enhancement methods.

This paper focuses on verification for reactive system specifications. A reactive system is an open system that continuously interacts with an uncontrollable external environment, and it must often be highly safe and reliable. However, realizability checking for a given specification is very costly, so we need effective methods to detect and analyze defects in unrealizable specifications to refine them efficiently. We introduce a systematic characterization on necessary conditions of realizability. This characterization is based on quantifications for inputs and outputs in early and late behaviors and reveals four essential aspects of realizability: exhaustivity, strategizability, preservability and stability. Additionally, the characterization derives new necessary conditions, which enable us to classify unrealizable specifications systematically and hierarchically.

Because processes run concurrently in multitask systems, the size of the state space grows exponentially. Therefore, it is not straightforward to formally verify that such systems enjoy desired properties. Real-time constrains make the formal verification more challenging. In this paper, we propose the following to address the challenge: (1) a way to model multitask real-time systems as observational transition systems (OTSs), a kind of state transition systems, (2) a way to describe their specifications in CafeOBJ, an algebraic specification language, and (3) a way to verify that such systems enjoy desired properties based on such formal specifications by writing proof scores, proof plans, in CafeOBJ. As a case study, we model Fischer's protocol, a well-known real-time mutual exclusion protocol, as an OTS, describe its specification in CafeOBJ, and verify that the protocol enjoys the mutual exclusion property when an arbitrary number of processes participates in the protocol*.

We consider the bisimilarity control problem for partially observed nondeterministic discrete event systems with deterministic specifications. This problem requires us to synthesize a supervisor that achieves bisimulation equivalence of the supervised system and the deterministic specification under partial observation. We present necessary and sufficient conditions for the existence of such a deterministic supervisor and show that these conditions can be verified polynomially.

In this letter, we propose a more secure modeling and simulation approach that can systematically detect state variable corruptions caused by buffer overflows in simulation models. Using our approach, developers may not consider secure coding practices related to the corruptions. We have implemented a prototype of the approach based on a modeling and simulation formalism and an open source simulator. Through optimization, the prototype could show better performance, compared to the original simulator, and detect state variable corruptions.

Many kinds of questionnaires, testing, and voting are performed in some completely electronic ways to do questions and answers on the Internet as Web applications, i.e. e-questionnaire systems, e-testing systems, and e-voting systems. Because there is no unified communication tool among the stakeholders of e-questionnaire, e-testing, and e-voting systems, until now, all the e-questionnaire, e-testing, and e-voting systems are designed, developed, used, and maintained in various ad hoc ways. As a result, the stakeholders are difficult to communicate to implement the systems, because there is neither an exhaustive requirement list to have a grasp of the overall e-questionnaire, e-testing, and e-voting systems nor a standardized terminology for these systems to avoid ambiguity. A general-purpose specification language to provide a unified description way for specifying various e-questionnaire, e-testing, and e-voting systems can solve the problems such that the stakeholders can refer to and use the complete requirements and standardized terminology for better communications, and can easily and unambiguously specify all the requirements of systems and services of e-questionnaire, e-testing, and e-voting, even can implement the systems. In this paper, we propose the first specification language, named “QSL,” with a standardized, consistent, and exhaustive list of requirements for specifying various e-questionnaire, e-testing, and e-voting systems such that the specifications can be used as the precondition of automatically generating e-questionnaire, e-testing, and e-voting systems. The paper presents our design addressing that QSL can specify all the requirements of various e-questionnaire, e-testing, and e-voting systems in a structured way, evaluates its effectiveness, performs real applications using QSL in case of e-questionnaire, e-testing, and e-voting systems, and shows various QSL applications for providing convenient QSL services to stakeholders.

Refinement-based formal specification is a promising approach to the increasing complexity of software systems, as demonstrated in the formal method Event-B. It allows stepwise modeling and verifying of complex systems with multiple steps at different abstraction levels. However, making changes is more difficult, as caution is necessary to avoid breaking the consistency between the steps. Judging whether a change is valid or not is a non-trivial task, as the logical dependency relationships between the modeling elements (predicates) are implicit and complex. In this paper, we propose a method for analyzing the impact of the changes of Event-B. By attaching labels to modeling elements (predicates), the method helps engineers understand how a model is structured and what needs to be modified to accomplish a change.

This paper demonstrates a PLL compiler that generates the final GDSII data from a specification of input and output frequencies with PVT corner conditions. A Pulse Width Controlled PLLs (PWPLL) is composed of digital blocks, and thus suitable for being designed using a standard cell library and being layed out with a commercially available place-and-route (P&R) tool. A PWPLL has 8 design parameters. Our PLL compiler decides the 8 parameters and confirms the PLL operation with the following functions: 1) calculates rough parameter values based on an analytical model, 2) generates SPICE and gate-level verilog netlists with given parameter values, 3) runs SPICE simulations and analyzes the waveform, to examine the oscillation frequency or the voltage of specified nodes at a given time, 4) changes the parameter values to an appropriate direction depending on the waveform analyses to obtain the optimized parameter values, 5) generates scripts that can be used in commercial design tools and invokes the tools with the gate-level verilog netlist to get the final LVS/DRC-verified GDSII data from a P&R and a verification tools, and finally 6) generates the necessary characteristic summary sheets from the post-layout SPICE simulations extracted from the GDSII. Our compiler was applied to an 0.18µm standard CMOS technology to design a PLL with 600MHz output, 600/16MHz input frequency, and confirms the PLL operation with 1.2mW power and 85µm×85µm layout area.

The software development process is front-loaded when formal specification is deployed and as a consequence more problems are identified and solved at an earlier point of time. This places extra importance on the quality and efficiency of the different formal specification tasks. We use the term “exploratory modeling” to denote the modeling that is conducted during the early stages of software development before the requirements are clearly understood. We believe tools that support not only rigorous but also flexible construction of the specification at the same time are helpful in such exploratory modeling phases. This paper presents a web-based IDE named VDMPad to demonstrate the concept of exploratory modeling. VDMPad has been evaluated by experienced professional VDM engineers from industry. The positive evaluation resulting from such industrial users are presented. It is believed that flexible and rigorous tools for exploratory modeling will help to improve the productivity of the industrial software developments by making the formal specification phase more efficient.

Verification of a design with respect to its requirement specification is important to prevent errors before constructing an actual implementation. The existing works focus on verifications where the specifications are described using temporal logics or using the same languages as that used to describe the designs. Our work considers cases where the specifications and the designs are described using different languages. To verify such cases, we propose a framework to check if a design conforms to its specification based on their simulation relation. Specifically, we define the semantics of the specifications and the designs commonly as labelled transition systems (LTSs). We appreciate LTSs since they could interpret information about the system and actions that the system may perform as well as the effect of these actions. Then, we check whether a design conforms to its specification based on the simulation relation of their LTS. In this paper, we present our framework for the verification of reactive systems, and we present the case where the specifications and the designs are described in Event-B and Promela/Spin, respectively. We also present two case studies with the results of several experiments to illustrate the applicability of our framework on practical systems.

In this paper, sequential prediction is studied. The typical assumptions about the probabilistic model in sequential prediction are following two cases. One is the case that a certain probabilistic model is given and the parameters are unknown. The other is the case that not a certain probabilistic model but a class of probabilistic models is given and the parameters are unknown. If there exist some parameters and some models such that the distributions that are identified by them equal the source distribution, an assumed model or a class of models can represent the source distribution. This case is called that specifiable condition is satisfied. In this study, the decision based on the Bayesian principle is made for a class of probabilistic models (not for a certain probabilistic model). The case that specifiable condition is not satisfied is studied. Then, the asymptotic behaviors of the cumulative logarithmic loss for individual sequence in the sense of almost sure convergence and the expected loss, i.e. redundancy are analyzed and the constant terms of the asymptotic equations are identified.

Survivability is an essential requirement of the networked information systems analogous to the dependability. The definition of survivability proposed by Knight in [16] provides a rigorous way to define the concept. However, the Knight's specification does not provide a behavior model of the system as well as a verification framework for determining the survivability of a system satisfying a given specification. This paper proposes a complete formal framework for specifying and verifying the concept of system survivability on the basis of Knight's research. A computable probabilistic model is proposed to specify the functions and services of a networked information system. A quantified survivability specification is proposed to indicate the requirement of the survivability. A probabilistic refinement relation is defined to determine the survivability of the system. The framework is then demonstrated with three case studies: the restaurant system (RES), the Warship Command and Control system (LWC) and the Command-and-Control (C2) system.

Many fatal accidents involving safety-critical reactive systems have occurred in unexpected situations that were not considered during the design and test phases of development. To prevent such accidents, reactive systems should be designed to respond appropriately to any request from an environment at any time. Verifying this property during the specification phase reduces development reworking. This property of a specification is commonly known as realizability. Realizability checking for reactive system specifications involves complex and intricate analysis. The complexity of realizability problems is 2EXPTIME-complete. To detect typical simple deficiencies in specifications efficiently, we introduce the notion of bounded strong satisfiability (a necessary condition for realizability), and present a method for checking this property. Bounded strong satisfiability is the property that, for all input patterns represented by loop structures of a given size k, there is a response that satisfies a given specification. We report a checking method based on a satisfiability solver, and show that the complexity of the bounded strong satisfiability problem is co-NEXPTIME-complete. Moreover, we report experimental results showing that our method is more efficient than existing approaches.

This paper introduces an ontology-based method for checking requirements specification. Requirements ontology is a knowledge structure that contains functional requirements (FR), attributes of FR and relations among FR. Requirements specification is compared with functional nodes in the requirements ontology, then rules are used to find errors in requirements. On the basis of the results, requirements team can ask questions to customers and correctly and efficiently revise requirements. To support this method, an ontology-based checking tool for verification of requirements has been developed. Finally, the requirements checking method is evaluated through an experiment.

Formalizing requirements in formal specifications is an effective way to deepen the understanding of the envisioned system and reduce ambiguities in the original requirements. However, it requires mathematical sophistication and considerable experience in using formal notations, which remains a challenge to many practitioners. To handle this challenge, this paper describes a pattern-based approach to facilitate the formalization of requirements. In this approach, a pattern system is pre-defined to guide requirements formalization where each pattern provides a specific solution for formalizing one kind of function into a formal expression. All of the patterns are classified and organized into a hierarchical structure according to the functions they can be used to formalize. The distinct characteristic of our approach is that all of the patterns are stored on computer as knowledge for creating effective guidance to facilitate the developer in requirements formalization; they are “understood” only by the computer but transparent to the developer. We also describe a prototype tool that supports the approach. It adopts Hierarchical Finite State Machine (HFSM) to represent the pattern knowledge and implements an algorithm for applying it to assist requirements formalization. Two experiments on the tool are presented to demonstrate the effectiveness of the approach.

A removable HDD “iVDR” is an international standardized medium, which has HDD features such as a large capacity and high-speed data transfer, and also is removable and compatible. We discuss the concepts of the hardware-specifications designed by the iVDR Consortium and the history of the international standardization activities for iVDR. We also discuss application expansions through these standardization activities.

Relay has been incorporated into standards of wireless access networks to improve the system capacity and coverage. However, the resource allocation problem to support scalable video coding (SVC) multicast for wireless relay networks is challenging due to the existence of relay stations (RSs). In this paper, we study the resource allocation problem for SVC multicast over multi-hop wireless relay networks to maximize the total utility of all users with a general non-negative, non-decreasing utility function. Since the problem is NP-hard, we simplify it with RS specification functions which specialize the relay station to receive data for each user, and convert the resource allocation problem with one RS specification function as finding a maximum spanning sub-tree of a directed graph under budget constraint. A heuristic algorithm is proposed to solve the problem with polynomial time complexity. The simulation results reveal that the proposed algorithm outperforms other algorithms under assumptions of two-hop wireless relay networks or separated transmission for relay and access links, and it keeps good approximation to the optimal results.

Many fatal accidents involving safety-critical reactive systems have occurred in unexpected situations, which were not considered during the design and test phases of system development. To prevent such accidents, reactive systems should be designed to respond appropriately to any request from an environment at any time. Verifying this property during the specification phase reduces the development costs of safety-critical reactive systems. This property of a specification is commonly known as realizability. The complexity of the realizability problem is 2EXPTIME-complete. We have introduced the concept of strong satisfiability, which is a necessary condition for realizability. Many practical unrealizable specifications are also strongly unsatisfiable. In this paper, we show that the complexity of the strong satisfiability problem is EXPSPACE-complete. This means that strong satisfiability offers the advantage of lower complexity for analysis, compared to realizability. Moreover, we show that the strong satisfiability problem remains EXPSPACE-complete even when only formulae with a temporal depth of at most 2 are allowed.

Digital RF solutions have been shown to be advantageous in various design aspects, such as accurate modeling, design reuse, and scaling when migrating to the next CMOS process node. Consequently, the majority of new low-cost and feature cell phones are now based on this approach. However, another equally important aspect of this approach to wireless transceiver SoC design, which is instrumental in allowing fast and low-cost productization, is in creating the inherent capability to assess performance and allow for low-cost built-in calibration and compensation, as well as characterization and final-testing. These internal capabilities can often rely solely on the SoCs existing processing resources, representing a zero cost adder, requiring only the development of the appropriate algorithms. This paper presents various examples of built-in measurements that have been demonstrated in wireless transceivers offered by Texas Instruments in recent years, based on the digital-RF processor (DRPTM) technology, and highlights the importance of the various types presented; built-in self-calibration and compensation, built-in self-characterization, and built-in self-testing (BiST). The accompanying statistical approach to the design and productization of such products is also discussed, and fundamental terms related with these, such as 'soft specifications', are defined.

This paper presents a strategy together with tool support for the translation of state machines from equational theories into rewrite theories, aiming at automatically generating rewrite theory specifications. Duplicate effort can be saved on specifying state machines both in equational theories and rewrite theories, when we incorporate the theorem proving facilities of CafeOBJ with the model checking facilities of Maude. Experimental results show that efficiencies of the generated specifications by the proposed strategy are significantly improved, compared with those that are generated by three other existing translation strategies.