Verification of temporal logic properties plays a crucial role in proving the desired behaviors of continuous systems. In this paper, we propose an interval method that verifies the properties described by a bounded signal temporal logic. We relax the problem so that if the verification process cannot succeed at the prescribed precision, it outputs an inconclusive result. The problem is solved by an efficient and rigorous monitoring algorithm. This algorithm performs a forward simulation of a continuous-time dynamical system, detects a set of time intervals in which the atomic propositions hold, and validates the property by propagating the time intervals. In each step, the continuous state at a certain time is enclosed by an interval vector that is proven to contain a unique solution. We experimentally demonstrate the utility of the proposed method in formal analysis of nonlinear and complex continuous systems.

In this paper, we propose two new falsification attacks against Wi-Fi Protected Access Temporal Key Integrity Protocol (WPA-TKIP). A previous realistic attack succeeds only for a network that supports IEEE 802.11e QoS features by both an access point (AP) and a client, and it has an execution time of 12–15 min, in which it recovers a message integrity code (MIC) key from an ARP packet. Our first attack reduces the execution time for recovering a MIC key. It can recover the MIC key within 7–8 min. Our second attack expands its targets that can be attacked. This attack focuses on a new vulnerability of QoS packet processing, and this vulnerability can remove the condition that the AP supports IEEE 802.11e. In addition, we discovered another vulnerability by which our attack succeeds under the condition that the chipset of the client supports IEEE 802.11e even if the client disables this standard through the OS. We demonstrate that chipsets developed by several kinds of vendors have the same vulnerability.

System implementation for e-Government initiatives should be reliable. Unreliable system implementation could, on the one hand, be insufficient to fulfill basic system requirements, and more seriously on the other hand, break the trust of citizens on governments. The objective of this paper is to advocate the use of formal methods in general, the OTS/CafeOBJ method in particular in this paper, to help develop reliable system implementation for e-Government initiatives. An experiment with the OTS/CafeOBJ method on an e-Government messaging framework proposed for providing citizens with seamless public services is described to back up our advocation. Two previously not well-clarified problems of the framework and their potential harm realized in this experiment are reported, and possible ways of revisions to the framework are suggested as well. The revisions are proved to be sufficient for making the framework satisfy certain desired properties.

This paper is intended as an investigation of scientific discoveries from a philosophical point of view. In the first half of this century, most of philosophers rather concentrated on the logical analysis of science and set the problem of discovery aside. Logical positivists distinguished a context of discovery from a context of justification and excluded the former from their analysis of scientific theories. Although Popper criticized their inductivism and suggested methodological falsificationism, he also left the elucidation of discovery to psychological inquiries. The problem of scientific discovery was proprely treated for the first time by the "New Philosophy of Science" school in the 1960's. Hanson reevaluated the method of "retroduction" on the basis of Peirce's logical theory and analysed Kepler's astronomical discovery in detail as a typical application of it. Kuhn's theory of paradigm located discoveries in the context of scientific revolutions. Moreover, he paid attention to the function of metaphor in scientific discoveries. Metaphorical use of existing terms and concepts to overcome theoretical difficulties often plays a decisive role in developping new ideas. In the period of scientific revolution, theoretical metaphors can open up new horizons of scientific research by way of juxtapositions of heterogeneous concepts. To explicate such a complicated situation we need the "rhetoric" of science rather than the "logic" of science.