This paper investigates that effect of neutral voltage on shaft voltages. The shaft voltages are expected to provide cause of bearing currents. The bearing currents damage bearing in motor. We expect neutral voltages to cause shaft voltages. Thus, we construct circuit of interior motor. And we predict generation of shaft voltages by simulation using the circuit. Then we measure the neutral voltage and draw a comparison between predictive value and measured value. As a result, we can confirm connections between shaft voltages and neutral voltages.

In various environments, such as mobile and wearable computing, compact I/O devices are desirable from the viewpoint of portability. Now, many users are accustomed to input with a keyboard, however, there is a limitation of miniaturization because it degrades the performance of key touch. Therefore, in this paper, we propose a method to miniaturize a keyboard by excluding the half of it. In using the proposed method, one hand hits keys as usual, and the other hand hits the place outside the keyboard as if the user types with both hands. The user can input words with only one hand because the proposed system estimates the input word using keying interval, which appears also when the user inputs with both hands. From the results of user study, we confirmed that the user can input with only one hand and that it does not decrease input speed drastically.

This paper presents a formal executable semantics of object-oriented models. We made it possible to conduct both simulation and theorem proving on the semantics by implementing it within the expressive intersection of the functional programming language ML and the theorem prover HOL. In this paper, we present the definition and implementation of the semantics. We also present a prototype verification tool ObjectLogic which supports simulation and theorem proving on the semantics. As a case study, we show the verification of a practical firewall system.

This paper proposes a different approach for service adaptation which aims to: (i) support non-regular adaptation; (ii) integrate adaptation and model checking. First, a pushdown automaton is used to model the adaptor so that non-regular languages are possible. Second, behavior interfaces of services are modeled by Büchi automata in order to take the advantage of the acceptance condition. By defining the property of ”behavior mismatch free” in a LTL formula using acceptance condition, the detection of behavior mismatches is performed by model checking. Also, the adaptor generation is performed by model checking of pushdown systems with the guidance of a special over-behavioral adaptor called “coordinator”. Then the returned counterexample is converted to a pushdown automaton, the expected adaptor.

In designing real time software, system designers need to find out the time budget to allocate to each action of real time tasks so that the tasks can meet their deadlines. Our solution to this problem involves representing the execution time of the actions as parameters, then analyzing the collaborative behavior of those real time tasks. This paper proposes parametric timed models of real time tasks whose executions are controlled by a scheduler. We develop an algorithm to synthesize a coherent model which represents the possible behavior from a set of real time tasks by exhaustively searching their reachable states. A set of linear inequalities are then derived on the fly from the synthesized model as the condition of parameters for schedulability. By solving the inequalities using a constraint solver, we can obtain desirable values of the parameters. In addition, we have implemented the algorithm in a tool and conducted some experiments to show the effectiveness of our approach.

Our society depend on embedded and ubiquitous computing and the reliability of embedded software becomes more and more important. We have conducted a five years project with industries to develop software for realizing highly reliable embedded systems. We have tackled reliability issues from the following aspects. (1)Design environment: we have developed a UML design verification tool that apply model checking techniques to improve the design quality of application software. (2)Operating environment: we have developed operating system supports that realize multiple execution of real-time operating systems and also developed operating systems with enhanced resource management. Both technologies contribute the realization of robust run-time environment. (3) Real-time environment: we have developed real-time garbage collection techniques for Jave. They prevent the suspension of applications that violates the correct behavior of real-time applications. Also, they reduce the effort of application programmers to avoid garbage-collection during important execution timing. We have obtained fruitful results from these three research themes, and some of them are actually used in industries. Furthermore, we have integrated the results to make synergetic effect of them. In order to demonstrate the effectiveness, we have conduct an experiment. In this paper, we introduce the project and its results.

This paper proposes a framework for verifying component-based software in the context of component evolution. This framework includes two stages: modular conformance testing for updating inaccurate model of the evolved component and modular verification for evolving component-based software. When a component is evolved after adapting some refinements, the proposed framework only focuses on this component and its model in order to update the model and recheck the whole evolved system. The framework also reuses the previous verification results and the previous models of the evolved component to reduce several steps of the model update and verification processes.

Generally, functions and execution environment which form a software system are changed because requirements change, referred to as "software evolution''. At this change, maintaining consistency of the configuration is important, in order to prevent trouble. However, it is difficult for software engineers to perform this kind of maintenance. Thus, when a configuration is changed, computer support is needed. In this paper, we propose a method of FMC (feature, module and connection) which focuses on the maintenance of configuration changes, and we formalize FMC by alloy. FMC is a modeling method which is based on the feature model of FODA. FMC abstracts functions, execution environment and correspondence relations between functions and execution environment. In addition, we describe how to check and correct inconsistency of FMC using alloy.

There are many kinds of events where participants converge and move around freely looking at points of interest. Since in these event spaces, the participants go where they want, some problems may arise for the event manager such as people staying in one area too long or congestion that occurs at specific attractions. Therefore, we propose here a new navigation system that has a route planning algorithm to satisfy the objectives of the event manager. In an actual test of our system, we found that the participants' actions were in line with the objectives of the event manager. Moreover, we also found that our system performs better by using wearable computing technologies because detailed information on participants is acquired.

Recently, design models that precise behavior of objects is specified are proposed. Though, currently, they are mainly used for their execution and automatic source code generation, they also have potential to allow us to verify them in the design phase. In this paper, we propose a method to verify such design models in the design phase. In addition, we adopt theorem proving systems to rigorously and efficiently verify it.

In this paper, we consider a distributed system that consists of a group of teams of worker robots that rely on physical robot messengers for the communication between the teams. Unlike traditional distributed systems, there is a finite amount of messengers in the system, and thus a team can send messages to other teams only when some messenger robot is available locally. It follows that a careful management of the messengers is necessary to avoid the starvation of some teams. Concretely, the paper proposes algorithms to provide group membership and view synchrony among robot teams. We look at the problem in the face of failures, in particular when a certain number of messenger robots can possibly crash.

Timing characteristic is a crucial point of concern in the design of real-time systems, because the systems are to operates under time-critical conditions. In this paper, we present a verification-driven approach for improving the correctness in the design of real-time systems. Our approach abstracts the details of timing information of the system by using time parameters. We propose parametric timed structure, an extension of timed transition systems, as a model for describing real-time systems. We define the parametric temporal logic PARCTL for specifying timing properties with time parameters. The model checking algorithms for parametric timed system are then proposed. The algorithms derive the necessary and sufficient condition over time parameters. We illustrate the application of our approach by deriving parameter conditions for a mutual exclusion protocol and show that the result of this approach can be used as guidelines for improving the timing correctness in the design of real-time systems.

For many years, people have been advocating the development of failure detection as a basic service, but, unfortunately, without meeting much success so far. We believe that this comes from the fact that important system engineering issues have not yet been addressed adequately, thus preventing the definition of a truly generic service. Ultimately, our goal is to define a service that is both simple and expressive, yet powerful enough to support the requirements of many distributed applications. To this end, we consider an alternative interaction model between the service and the applications, called accrual failure detectors. Roughly, an accrual failure detector associates to each process a real value representing a suspicion level, instead of the traditional binary information (i.e., trust vs. suspect). In this paper, we provide a rigorous definition for accrual failure detectors, demonstrate that changing the interaction model leads to no loss in computational power, discuss quality of service issues, and present several possible implementations.

In the upstream phase of object-oriented development, we usually model a target system from multiple points of view. A dataflow view has been recognized as one of the most important views in software engineering. We need to relate dataflow models to OO models and check consistency between them as it is still important even if we adopt object-oriented approach. In this paper, we propose a method to analyze dataflows in OO design models with the model checker Spin after formalizing them.

Scheduling divisible workloads in distributed systems has been one of the interesting research problems over the last few years. Most of the scheduling algorithms previously introduced are based on the master-worker model. However, the majority of these algorithms assume that workers are dedicated machines, which is a wrong assumption in distributed environments such as Grids. In this work, we propose a dynamic scheduling methodology that takes into account the three prominent aspects of Grids: heterogeneity, dynamicity, and uncertainty. Our contribution is threefold. First, we present an analytical model for processing local and Grid tasks at each non-dedicated worker. Second, we present a simple prediction method to forecast the available CPU capacity and bandwidth at each worker. Third, we introduce a dynamic, multi-round scheduling algorithm.

The detection of failures is a fundamental issue for fault-tolerance in distributed systems. Recently, many people have come to realize that failure detection ought to be provided as some form of generic service, similar to IP address lookup or time synchronization. However, this has not been successful so far; one of the reasons being the fact that classical failure detectors were not designed to satisfy several application requirements simultaneously. We present a novel abstraction, called accrual failure detectors, that emphasizes flexibility and expressiveness and can serve as a basic building block to implementing failure detectors in distributed systems. Instead of providing information of a binary nature (trust vs. suspect), accrual failure detectors output a suspicion level on a continuous scale. The principal merit of this approach is that it favors a nearly complete decoupling between application requirements and the monitoring of the environment. In this paper, we describe an implementation of such an accrual failure detector, that we call the /spl phi/ failure detector. The particularity of the /spl phi/ failure detector is that it dynamically adjusts to current network conditions the scale on which the suspicion level is expressed. We analyzed the behavior of our /spl phi/ failure detector over an intercontinental communication link over a week. Our experimental results show that if performs equally well as other known adaptive failure detection mechanisms, with an improved flexibility.

Protocols that solve agreement problems are essential building blocks for fault tolerant distributed systems. While many protocols have been published, little has been done to analyze their performance, especially the performance of their fault tolerance mechanisms. In this paper, we compare two well-known asynchronous consensus algorithms. In both algorithms, a leader process tries to impose a decision, and another leader retries if the leader fails doing so. The algorithms elect leaders differently: the Chandra-Toueg algorithm has a rotating leader, whereas processes in the Paxos algorithm elect leaders directly. We investigate the performance implications of this difference. In the system under study, processes send atomic broadcasts to each other. Consensus is used to decide the delivery order of messages. We evaluate the steady state latency in (1) runs with neither crashes nor suspicions, (2) runs with crashes and (3) runs with no crashes in which correct processes are wrongly suspected to have crashed, as well as the transient latency after (4) one crash and (5) multiple correlated crashes. The results show that the Paxos algorithm tolerates frequent wrong suspicions (3) and correlated crashes (5) better, while the performance is comparable in all other scenarios.

Software is subject to change. Changes come from many sources. It has to change as its infrastructure has been changed. It has to change as its functionality has to be augmented. It has to change as new algorithms are found which will increase it performance. There are a lot of reasons why it has to change and only software which can stand for the change can survive. Changes which are gradual and put it into a desirable form is called evolution. This kind of change is essential in constructing a complex software system. Really, it could only be constructed as a result of repeated changes applied to the initial system. Changes are thus common in software development and much work has been done so far producing many important ideas and concepts. Still, changing software reasonably and effectively is not an easy task. This is by the lack of leading principles for the changes and the inherent difficulties of the changes. If we can find them our understanding and practices of changing software will be greatly advanced. The author has introduced a seemingly fundamental concept for scientific treatment of software change problems has been introduce, which is called evolutionary domain. This is a set of objects together with an order relation, called an evolutionary relation, and a difference operator on them. In this talk, I am going to investigate on several current practices and methods for software evolution on this proposed basis, such as components and patterns in OO methodology, feature/collaboration/aspect-oriented development, and MDA approach which is a current highlight of UML based development. Despite the above methods and practices, software evolution is still hard. It is due to the inherently difficult problem of anticipating changes. Anticipation of changes is usually hard and needs understanding of the world where software is used. We need to know what kind of specifications or requirements for software are permissible there and how they are described. Also we need to how to define their difference to make one to evolve to others. This is where the evolutionary domain concept could be applied. As an example, Object Logic, which is build on a higher order logic HOL, is introduced for describing an object-oriented world and for showing how evolutionary relation could be defined on thus defined world.

We propose an environment for evolutionary prototyping technique, which is a theoretical framework based on abstract interpretation for Java programs. In general, it is difficult to execute a prototype in the intermediate stage of top-down development. This disadvantage prevents us to find bugs in the early stage of the development. The technique we propose here allows programmers to execute the prototype as a whole, even though it is partially implemented. In the technique, an object is repeatedly changed with interface changes. Our idea is to use an earlier runnable object instead of an unimplemented later object in runtime. The changes of objects are based on abstract interpretation. However, it is necessary to realize the mechanism for using the alternative object including the interface changes in Java. To solve this problem, we introduce proxy object, which is a mediator containing all interface and transform objects dynamically and automatically to keep execution going. Moreover, proxy objects can be automatically generated by the dynamic proxy class API, which is one of Java reflection mechanism. As a result, our environment would reduce the cost that programmers describe code for adjusting current objects.

Collaboration-based designs [K. Fisler et al. (2001), T. T. Nguyen et al. (2003), Y. Smaragdakis et al. (1998)] are an effective software development approach due to its achievement in separation of concerns [G. Kiczales et al., (1997), P. Tarr et al. (1999)]. These designs also demand a new model checking technique allowing to prove system correctness by verifying each collaboration individually with a minimum assumption about other collaborations. To verify a collaboration of multiple actors, a typical technique consists of constructing a standard cross-product of actor statecharts as global state space and then checking properties with respect to that global space. We initially point out some drawbacks of a previous approach [K. Fisler et al. (2001)] in verifying collaboration. Then, in addition to intra-object behaviors in statecharts as of [K. Fisler et al. (2001)], we first improve the technique by imposing additional constraints to model checking process via protocol invariants which are essentially inter-object behaviors. Due to these additional constraints, state space is reduced and more importantly, our model reflects more accurately about system behavior by eliminating those unreachable states. Second, a more general form, i.e. multiple exit and re-entry states, of the interface between two collaborations is used instead of a fixed interface with single exit and re-entry states. Some pre-processing work on reentry states and solutions to specifics of properties to be verified are also discussed regarding to the soundness of the verification algorithm.

The aim of this paper is to demonstrate the significance of XML semantics checker approach. We apply this novel approach to check the semantic consistencies of the Quran holy book that is mentioned by Jon Bosak in Religion 2.00 Web site. Religion 2.00 is a group of four religious works marked up for electronic publication from publicly available sources. In this paper, we will concentrate mainly on studying the case study of the Quran holy book that is mentioned in the previous web site. We successfully applied our approach of XML semantics to check that the number of verses in each chapter was correctly written in the Quran XML format document. We also checked that the Quran XML document contains exactly the same number of chapters as in the real Quran holy book. In addition, we computed automatically the total number of verses in the holy book.

As a result of the increasing size and complexity of embedded systems, object-oriented techniques are going to be adopted in the embedded software development. In embedded software developments, we have to consider non-functional requirements such as real-time properties and resource requirements. To deal with these requirements, some methodologies design the system using a thread-based approach. In such approach, we need to extract threads from the concurrent objects defined in the analysis model. However, current methodologies do not provide enough support to do so. We propose a formal approach to extract threads from concurrent objects. We also present an experimental application of the proposed approach to the development of a device driver.

We address the problem of checking the consistency of the semantics associated with an eXtensible Markup Language (XML) document. We propose a new technique to implement the incremental attribute evaluation approach to check the consistency of XML documents from the semantics point of view. In a previous paper, we have proposed a new technique to add semantics to XML documents by attaching the semantics information to the XML element tag attributes. This approach is based on the same concept as in attribute grammars (AGs) by attaching and checking static semantics of programming languages through their attributes. We extend our work by adding incremental facilities to the proposed evaluator. By introducing the incremental approach to our technique we improve its efficiency by minimizing the re-evaluation process. Only the affected areas in the XML document are re-evaluated rather than re-evaluating the whole document.

This paper discusses the problem of implementing a scalable failure detection service for grid systems. More specifically, traditional implementations of failure detectors are often tuned for running over local networks and fail to address important problems found in wide-area distributed systems, such as grid systems. We identify some of the most important problems raised in the context of grids. We then survey recent propositions that can help in solving some of these problems.

It is important to design architecture to be steady throughout the evolution, or make the architecture to be the platform for a product family. In order to design software architecture to have such characteristics we have to analyze the commonality and differences among requirements on potential software that are supposed to be developed on the architecture, and then design software architecture so as to accommodate the commonality and differences. In this paper, we propose an approach for architectural design in which we analyze the requirements of potential software in terms of the impact on the architecture, considering multiple quality attributes. We perform a case study on an actual project that designed architecture for an on-board system for ITS systems to examine the usefulness of the technique. We also apply the technique to the same architectural design problem to demonstrate that it is applicable to the real problem.

The scale of software products is becoming larger as a result of the rapid progress and increasing use of computer systems. It is necessary to develop such large-scale software effectively. object-oriented methodologies have been proposed for the development of such systems. In typical object-oriented methodologies like OMT, a target system is described by several model which mirror different views of it. Though it is desirable to analyze models in this style as it enables us to represent independent aspects of the system in orthogonal manner, it causes a difficulty to maintain consistency among them. In this paper, we show a mechanism to unify analysis models at first. This allows us to deal with the models in concepts shared by them. Next we propose a verification method for checking consistency among them with respect to dataflow. In our method, verification is performed by proving dataflow in an axiomatic system.

Presents a replication technique based on the FTAG (fault-tolerant attribute grammar) computation model, where instances of a replicated application are active on different groups of processors called replicas. FTAG is a functional and attribute-based model. The developed replication technique implements "active parallel replication", i.e. all replicas are active and concurrently compute a different piece of the application's parallel code. In our model, replicas cooperate not only to detect and mask failures but also to perform parallel computation. The replication mechanisms are supported by the FTAG run-time system and are fully application-transparent. Different novel mechanisms for checkpointing and recovery are developed. Rollback is achieved only if the system experiences multiple failures, otherwise forward recovery is performed. The replication technique takes full advantage of parallel computation to reduce the computation time.

The design procedures for a typical real-time processing system (the checkout system for an artificial spacecraft) were analyzed by experienced engineers using the hierarchical functional software process (HFSP) model and attaching importance to time elapse in design work. Another team was formed to design another design problem, reusing the software process, and evaluating it. It is shown that a new set of software processes which have broad adaptability can be obtained.>

Article A hierarchical and functional software process description and its enaction Share on Author: Takuya Katayama Department of Computer Science, Tokyo Institute of Technology, 2-12-1, Ookayama Meguro-ku Tokyo Japan 152 Department of Computer Science, Tokyo Institute of Technology, 2-12-1, Ookayama Meguro-ku Tokyo Japan 152View Profile Authors Info & Claims ICSE '89: Proceedings of the 11th international conference on Software engineeringMay 1989 Pages 343–352https://doi.org/10.1145/74587.74632Online:15 May 1989Publication History 73citation489DownloadsMetricsTotal Citations73Total Downloads489Last 12 Months4Last 6 weeks1 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 SiteGet Access

Global storage allocation for attributes in an attribute grammar evaluator is discussed and an algorithm for determining if a given set of attribute occurrences can share a common global storage is obtained.

An efficient method for evaluating attribute grammars by translating them into sets of procedures is presented.The basic idea behind the method is to consider nonterminal symbols of the grammar as functions that map their inherited attributes to their synthesized attributes.Associated with the nonterminal symbols are procedures that realize the functions.The attribute grammar is translated into a program consisting of these procedures.The essential point about this method is that attribute grammars are completely compiled into procedures, in contrast with evaluation algorithms that work interpretively in a table-driven manner.No information is stored in the nodes of derivation trees.Although this evaluation method is applicable principally to absolutely noncircular attribute grammars in which the dependency relation among attribute occurrences of every production rule does not contain cycles, it is shown how the method is extended to the general noncircular attribute grammars.Problems of evaluating a set of attributes simultaneously and of recursive descent evaluation are also discussed.

Verification of attribute grammar is discussed. As is widely recognized, attribute grammar of Knuth [8] is a very convenient device to describe semantics of programming languages, especially in automating compiler construction. Many efforts have been made to obtain efficient evaluators for attribute grammar [1,3,4,5,7,10] so that efficient compilers may be produced from the semantic specifications written in the attribute grammar.There is another important problem about the semantic specifications. This is how to verify the correctness of the specification and is essential in ascertaining the correctness of produced compilers. In contrast with the evaluation problem, this has not been studied well and only a few partial results have been reported up to now [2,9].In this paper we propose a verification procedure for proving the correctness of attribute grammar, which is applicable to the wide class of attribute grammars called absolutely noncircular ones [7]. Our method can be extended to accept any noncircular attribute grammar since it is shown that any noncircular attribute grammar is transformed into an equivalent absolutely noncircular one [5].Our verification procedure utilizes dependency relations among attributes and verification is performed by induction based on this order relation, according to which attributes are evaluated. This procedure consists of (1) assigning assertions to relevant pairs of a nonterminal symbol and a parallelly evaluable subset of its attributes, (2) generating a set of verification conditions for each production rule with the aid of dependency graph of the rule and (3) proving the verification conditions. Of course, verification is performed production-rule-wise.Our method can accept attribute grammars which contain both synthesized and inherited attributes and handle them in a well-formed way. This contrasts to the previous works where only the synthesized case is considered [2] or there seems no general and formal descriptions about how to verify general attribute grammars [9].In this paper we first give necessary definitions and notations for attribute grammar and then propose a verification procedure to prove its correctness. After giving some examples of verification, we establish consistency and completeness of our procedure.