■Faculty | Department of Informatics |

■Position | Professor |

■Degree | |

■Commentator Guide | https://www.kindai.ac.jp/meikan/443-higuchi-masahiro.html |

■URL | |

Last Updated :2020/09/30

- 2013 04 , - 現在, Faculty of Science and Engineering, Kindai University
- 2000 04 , - 2013 03 , Faculty of Science and Engineering, Kindai University

- Informatics, Software

- A Handling Management System for Freight with the Multiple Ambient Calculus and UHF RFID Tags, Takahiro Hashimoto, Toru Kato, Masahiro Higuchi, 情報処理学会論文誌. プログラミング, 情報処理学会論文誌. プログラミング, 6(2), 1 - 12, Aug. 29 2013 Summary:We are investigating a way of modeling freight system in the Multiple Ambient Calculus (MAC) and the management systems ensuring the correctness of container handling during shipping using the model. Freight systems have nested structures, i.e., packages (e.g. containers) containing smaller packages (e.g. luggage) that are accommodated by a larger entity such as a container ship. MAC is a formal description language that is suitable for modeling such systems with the nested structures that dynamically change. Using MAC, whole the freight system is modeled by a set of formulae each of which represents the handling of each containers while, using the Ambient Calculus, the freight systems are modeled by a large formula. Thanks to this feature of MAC, we can express symmetric and concurrent property of freight systems more appropriately and adding or retracting formulae (representing adding or canceling containers for a voyage) becomes easier than using AC. The management system propsesed in this paper consists of three sub systems. The first generates formulae that represent freight systems based on several trading documents, the second deploys the formulae to each devices (PCs and RFID tags), the last senses the handling of containers by using UHF RFID devices and checks their consistency with the transitions of corresponding formulae. We also show the results of preliminary experiments in which a car is used as a container.
- An Ambient Logic Model Checking System for Freight Systems, Toru Kato, Masahiro Higuchi, Naoto Ueda, 情報処理学会論文誌. 数理モデル化と応用, 情報処理学会論文誌. 数理モデル化と応用, 3(1), 73 - 86, Jan. 26 2010 Summary:We present a variant of Ambient Logic to describe desired properties of freight systems and a model checking algorithm for the logic. In the field of distribution, the increase in cargo handling errors is a serious problem as the amount of freight circulation increases. We study a freight inspection system based on Ambient Calculus and we have already built a prototype system. The system can derive process formulas from several freight documents. The system also checks that the actual freight movement conforms the derived formula. To show the correctness of freights transportation, we have to ensure the validity of process formula. We provide an Ambient Logic to present desired properties of freight systems, such as "every cargo will be eventually transported to its destination". We also present an algorithm to show process formula satisfy Ambient Logic formula by exploring state transition graph. We conducted a verification experiment using the model checking system.
- A Conformance Decision System for Physical Distribution with the Ambient Calculus, MORIMOTO DAISUKE, KATO TORU, HIGUCHI MASAHIRO, 情報処理学会論文誌. プログラミング, 情報処理学会論文誌. プログラミング, 48(10), 151 - 164, Jun. 15 2007 Summary:In the field of distribution, an increasing of the handling fault of luggage becomes serious problem while the amount of circulation of the freight increases. To solve the problem, we are researching on the constructing the distribution management system based on descriptions of the physical distribution system in the Ambient Calculus. The physical distribution system has the layered structure, e.g., packages (e.g., container) including smaller packages (e.g., luggage) are accommodated by larger entity such as container ships and so on. On the other hand, the Ambient Calculus is a formal description language suitable for representing systems whose layered structure dynamically changes. This feature enables us to express concisely physical distribution systems. The validity of the description can be formally verified with a system of axioms for Ambient Logic. We propose the automatic generating system of the Ambient Calculus formulae, and conformance decision system for the movement of actual freights. The former system generates the formulae that express the transportation route of containers based on the shipping invoice written in Excel files used in an actual container shipping. The latter system checks the movement of an actual freight by comparing it with transition of the formulae. We also present the result of simple experiments to show the effectiveness of those systems.
- A Method to Generate Test Sequences for DFSM Protocol with Timer System Call(Special Issue on Multimedia Communication Systems), MORI TAKANORI, TOKUDA KOHEI, TADA HARUMASA, HIGUCHI MASAHIRO, HIGASHINO TERUO, IPSJ Journal, IPSJ Journal, 42(12), 3072 - 3081, Dec. 15 2001 Summary:In this paper, we propose a method to generate test sequences for communication protocols modeled as DFSM with timers. The test sequences can detect any single fault of timer commands or destination states in the transitions on protocol machines. For each single timer command fault, we give sufficient conditions that a given IUT is (or is not) equivalent to its specification. Based on these sufficient conditions, we give a method for generating test sequences. For each destination state fault, we give a test sequence generation method based on Wp-method. To show the usefulness of this method, we developed a system for generating test sequences, and applied it to DHCP (Dynamic Host Configuration Protocol). As a result, we generated the test sequences efficiently.
- Conformance Testing for Communication Protocols Modeled as Concurrent DFSMs with Non-observable Non-deterministic Behavior(Special Issue on Multimedia Communication Systems), FUKADA ATSUSHI, MORI TAKANORI, NAKATA AKIO, KITAMICHI JUNJI, HIGUCHI MASAHIRO, HIGASHINO TERUO, IPSJ Journal, IPSJ Journal, 42(12), 3063 - 3071, Dec. 15 2001 Summary:According to the progress of high-speed networks, many communication protocols are specified as concurrent systems. Such systems can be modeled as concurrent deterministic FSMs (DFSMs). In those protocols, a common input may be taken by some of concurrent DFSMs competitively (non-deterministically). In such a case, the global behavior becomes non-observable non-deterministic in general. In this paper, we propose a conformance testing method based on GWp-method for a sub-class of non-observable non-deterministic FSMs (NFSMs). The proposed method can be used not only for testing NFSMs directly but also for testing concurrent DFSMs whose global behavior is non-observable non-deterministic.
- An Event Abstraction Method in Distributed Computations Based on Control Flow (Special Issue on Multimedia Network System), TADA HARUMASA, HIGUCHI MASAHIRO, IPSJ Journal, IPSJ Journal, 42(2), 260 - 267, Feb. 15 2001 Summary:In this paper, we propose a simplification method of structure of distributed computations. In general, distributed computations are modeled as partial ordered events. In order to facilitate analysis of distributed computations, event abstraction has been proposed. Event abstraction reduces apparent complexity of a distributed computation by replacing some related events with one abstract event. The existing method of event abstraction is difficult to use because an analyzer should grasp the structure of the distributed computation. We classified the causal relation of events into two types, that is, the control dependency and the data dependency. Then, we defined the control flow based on the control dependency. In the proposed method, closed control flows are extracted from the distributed computation. Since each closed control flow can be considered as a module in the execution, events involved in a closed control flow are replaced with an abstracted event. To evaluate the proposed method, we implemented a visualization tool of distributed computations based on the method. We applied the tool to some of distributed programs and showed that the proposed method is useful for detecting some kind of programming errors.
- A Hierachical-Keyword-based Naming Scheme in File Systems, 42(9), 2328 - 2338, 2001
- A Fault Coverage Evaluation of Test Suite Generation Methods for EFSM, KOHARA MASARU, MORI TAKANORI, HIGUCHI MASAHIRO, FUJII MAMORU, IPSJ Journal, IPSJ Journal, 40(7), 3113 - 3116, Jul. 15 1999 Summary:In 4), a test suite generation method for communication protocols modeled as Finite-State Machine with Counters, a subclass of Extended Finite-State Machine (EFSM), is proposed. In this paper, a practical evaluation of fault detection power of test suites generated by the method and several other test generation methods. For the evaluation, we developed a mutation system which derives implementations with single or double faults from correct protocol implementation in C program. We examined whether the test suites can detect faults in the derived mutations. The experiment has shown that the fault coverage of the method proposed in 4) is superior to other methods.
- A Method for Generating Test Cases for Register Operations in Conformance Testing of Communication Protocols(<特集>Special Issue on New Generation Database Technology for Internet, Multimedia and Mobile computing), HIGUCHI MASAHIRO, KOHARA MASARU, NAKAISHI TAKAHARU, FUJII MAMORU, IPSJ Journal, IPSJ Journal, 39(4), 1067 - 1076, Apr. 15 1998 Summary:In this paper, we propose a condition of test cases for communication protocols modeled as FSM with counters(FSM-C), a subclass of Extended Finite-State Machines(EFSM). By using test cases satisfing the proposing condition, single fault of on determinig inequality or register assignments can be detected. We also propose a procedure to find test cases which satisfy the condition. To see the usefulness of this method, we developed a test cases generating system based on the proposing method, and applied the system to the OSI session protocol. As a result we can verify that all of test cases are generated automatically.
- Semi-automatic Generation of Invariant Formula for Verifying Communication Protocols Modeled as ECFSMs, HIGUCHI Masahiro, SANO Junko, HARA Keigo, FUJII Mamoru, The transactions of the Institute of Electronics, Information and Communication Engineers, The transactions of the Institute of Electronics, Information and Communication Engineers, 80(4), 179 - 188, Apr. 25 1997
- A Phase Connection Method for Communication Protocols, Sano Tetsuo, Higuchi Masahiro, Seki Hiroyuki, Kasami Tadao, The transactions of the Institute of Electronics, Information and Communication Engineers, The transactions of the Institute of Electronics, Information and Communication Engineers, 78(6), 519 - 531, Jun. 25 1995
- A Verification Method for Liveness of Communication Protocols Modeled as ECFSMs, Sugawa Satoshi, Higuchi Masahiro, Fujii Mamoru, The transactions of the Institute of Electronics, Information and Communication Engineers, The transactions of the Institute of Electronics, Information and Communication Engineers, 78(1), 17 - 28, Jan. 25 1995

- Timed Ambient Calculus, 2013 01
- 2D-data partition on the Heterogeneous BSP model, The International Association of Science and Technology for Development (IASTED), 2003 11 , The International Association of Science and Technology for Development (IASTED)
- A File Naming Scheme using Hierachical Keywords, 26th International Computer Software and Applications Conference（Compsac2002） （Oxford）, 2002 08 , 26th International Computer Software and Applications Conference（Compsac2002） （Oxford）

- The Timed Ambient Calculus, Masahiro Higuchi, 6, 2, 2013 08 29 , http://ci.nii.ac.jp/naid/110009602867Summary:In this presentation, we propose the timed ambient calculus as an extention of the ambient calculus. The ambient calculus is a process algebra suitable for specifying systems, which contain dynamically changing nested structures. By the benefit of such a feature, the ambient calculus is also suitable for modeling physical object distribution systems, such as maritime logistics. For modeling actual distribution systems, it is desirable that the specification includes timing constraints. We introduce i) capabilities with expiration time, ii) waiting capability, and iii) special ambient that expresses the timing violation, into the ambient calculus. We give the syntax and reduction rules for such capabilities and ambients in addition to the ones of the original ambient calculus. We can specify the lower limit and upper limit of the timing interval between two events, and timeout-like behavior using the timed ambient calculus. We also describe distribution monitoring systems based on a timed ambient calculus specification, and some macro notations for the convenience of describing complex systems.
- B-002 Automatic generation of high coverage unit test for Web-applications, Kamada Takayuki, Higuchi Masahiro, 10, 1, 245, 246, 2011 09 07 , http://ci.nii.ac.jp/naid/110009623283
- 3P-9 Evalution of Object Distribution Method using Low Traffic Quorum System for Mobile Ad Hoc Network, Michibata Shinnosuke, Moriya Sen, Higuchi Masahiro, 72, 1, "1, 491"-"1-492", 2010 03 08 , http://ci.nii.ac.jp/naid/110008105572
- A Management System for Freight Systems with Dynamic Routing based on the Ambient Calculus, Toshinobu Tsujimura, Masahiro Higuchi, Toru Kato, IPSJ SIG Notes, 2010, 35, 1, 6, 2010 02 25 , http://ci.nii.ac.jp/naid/110007993881Summary:We are investigating freight management systems ensuring the correctness of container handling during shipping. Such systems determine the correctness by comparing container handling, which is sensed by RFID, with transitions of formal models (formulae) written in the Ambient Calculus. Freight systems have the nested structures, i.e., packages (e.g. containers) containing smaller packages (e.g. luggage) that are accommodated by a larger entity such as a container ship. The Ambient Calculus is a formal description language that is suitable for modeling systems with the nested structures that dynamically change. The management system consists of two components: a system that automatically generates formulae of the Ambient Calculus and another system that manages the actual freight. The former system generates formulae that express the transportation routes of containers based on several trading documents such as shipping invoices, B/L instructions and routing plan tables of ships. The latter system senses the movement of containers by using RFID and checks their consistency with the transitions of corresponding formulae. The management system can treat hub and spoke type freight systems where containers leave a spoke port for another spoke port via more than one hub port that are recently becoming common.
- An Ambient Logic Model Checking System For Freight Systems, Toru Kato, Masahiro Higuchi, Naoto Ueda, IPSJ SIG Notes, 2009, 29, 1, 6, 2009 09 03 , http://ci.nii.ac.jp/naid/110007993845Summary:We present a variant of Ambient Logic to describe desired properties of freight systems and a model checking algorithm for the logic. In the field of distribution, the increase in cargo handling errors is a serious problem as the amount of freight circulation increases. We study a freight inspection system based on Ambient Calculus and we have already built a prototype system. The system can derive process formulas from several freight documents. The System also checks that the actual freight movement conforms the derived formula. To show the correctness of freights transportation, we have to ensure the validity of process formula. We provide an Ambient Logic to present desired properties of freight systems, such as "every cargo will be eventually transported to its destination". We also present an algorithm to show process formula satisfy Ambient Logic formula by exploring state transition graph. We conducted a verification experiment using the model checking system.
- An Ambient Logic Model Checking System for Freight Systems, Naoto Ueda, Toru Kato, Masahiro Higuchi, 2, 3, 2009 07 10 , http://ci.nii.ac.jp/naid/110007970912Summary:We present a variant of Ambient Logic to describe desired properties of freight systems and a model checking algorithm for the logic. In the field of freight distribution, the cargo handling fault problem becomes serious while the amount of circulation of the freights increases. We study a freight inspection system based on Ambient Calculus and we have already built a prototype system. The system can derive process formulas from several freight documents. The System also checks that the actual freight movement conforms the derived formula. To show the correctness of freights transportation, we have to ensure the validity of process formula. We provide an Ambient Logic to present desired properties of freight systems, such as "every cargo will be eventually transported to its destination". We also present an algorithm to show process formula satisfy Ambient Logic formula by exploring state transition graph. We conducted a verification experiment using the model checking system.
- 3M-7 Implementation of A Conformance Decision System for Physical Distribution with the Ambient Calculus, Tsujimura Toshinobu, Kato Toru, Higuchi Masahiro, 71, 1, "1, 385"-"1-386", 2009 03 10 , http://ci.nii.ac.jp/naid/110007502086
- RA-005 Model Checking for Ambient Calculus Description of Freight System, Ueda Naoto, Kato Toru, Higuchi Masahiro, 7, 1, 13, 16, 2008 08 20 , http://ci.nii.ac.jp/naid/110007641147
- A Translation System of Java Distributed Objects into π-Processes, Takafumi Kai, Toru Kato, Masahiro Higuchi, 1, 1, 2008 06 26 , http://ci.nii.ac.jp/naid/110007970847Summary:We introduce a translation system of distributed applications into processes of the π-calculus, assuming that distributed applications are written in Java using RMI. Such translations make it possible to apply formal methods, e.g. model checking by MWB or Pi-ET, to various practical distributed applications. In applications using Java RMI, mutual referencing relation among distributed objects can be dynamically changed by passing object's references. Also in the π-calculus, communication links connecting processes can be dynamically changed by passing port names. We focus on such a similarity and considered that the π-calculus is suitable as a formal computing model for distributed applications using Java RMI. Since method invocation and constructor invocation in Java applications are executed in terms of message passing, our system translates these invocations into I/O actions of the π-calculus. Our system also translates Java's conditional statements into π-processes having match and mismatch operators, and Java's loops and data structures such as map into recursively defined processes. To show the usefulness of such translations, we conducted an experiment of applying a distributed chat system to our translation system. The chat system consists of a server and 2 or more chat clients, written with Java RMI. Each client can obtain the other client's reference by requesting to the server.
- D-1-12 State space reduction in translating timed automaton into FSM with timers, Takeuchi Tsuyoshi, Higuchi Masahiro, Proceedings of the IEICE General Conference, 2008, 1, 2008 03 05 , http://ci.nii.ac.jp/naid/110006868005
- A-032 A Translation System of Distributed Objects into Pi-Processes, Kai Takafumi, Kato Toru, Higuchi Masahiro, 6, 1, 75, 76, 2007 08 22 , http://ci.nii.ac.jp/naid/110007685116
- M-014 A fault recovering method for distributed system with timer preserving timed causal order, Matsumoto Shinji, Higuchi Masahiro, 6, 4, 165, 166, 2007 08 22 , http://ci.nii.ac.jp/naid/110007688918
- A_014 On Translating Timed Automata into FSM with Timer, Okada Ryo, Higuchi Masahiro, 5, 1, 29, 30, 2006 08 21 , http://ci.nii.ac.jp/naid/110007684641
- On Translation of Distributed Applications with ORB Technology into Pi-processes, YAMAGUCHI MASASHI, KATO TORU, HIGUCHI MASAHIRO, 47, 11, 2006 07 15 , http://ci.nii.ac.jp/naid/110006390846
- A-015 Descripting Java Programs with dynamic link and Translating them into π-processes, Yamaguchi Masashi, Kato Toru, Higuchi Masahiro, 4, 1, 37, 38, 2005 08 22 , http://ci.nii.ac.jp/naid/110007684372
- 2D-data partition on the Hetetogeneous BSP model, ISHIMIZU Takashi, HIGUCHI Masahiro, FUJIWARA Akihiro, MASUZAWA Toshimitsu, IEICE technical report. Theoretical foundations of Computing, 102, 343, 1, 7, 2002 09 23 , http://ci.nii.ac.jp/naid/110003191981Summary:The HBSP(Heterogeneous Bulk-Synchronous Parallel) model is an asynchronous parallel computing model, whose communication features are abstracted by some parameters. In this paper, we propose two algorithms for the 2D-data partition and the matrix multiplication whose size is n × n. On the p processor HBSP model, the 2D-data partition algorithm allocates O(n^2s_i/?^<p-1>_<k=0>sk) data for each processor P_i accoding to its speed s_i, and the total of length and breadth of the partitions is O(n√<p>), and the matrix multiplication algorithm runs in O(n^3/?^<p-1>_<k=0>sk + L) computation time and in O((n^2√<p>/?^<p-1>_<k=0>sk+p/so)g + L), communication time.
- A Verification Procedure for Systems Modeled as Finite State Machines with Timers, Tokuda Kouhei, Mori Takanori, Higuchi Masahiro, Taniguchi Kenichi, IPSJ SIG Notes, 2001, 15, 85, 90, 2001 02 20 , http://ci.nii.ac.jp/naid/110004028859Summary:In this paper, we discuss a verification procedure for systems modeled as finite state machines with timers. We can verify such systems enumerating reachable states of the system from the initial state. If timers can store large integer value, it is troublesome to enumerate reachable states because of the large number of states of the system. We propose a procedure to enumerate reachable states of such system efficiently with simultaneous inequalities. We develop a verification system based on the proposing procedure, and apply to DHCP. As a result, the verification was executed in practical time.
- A Keyword Management Method on Hierarchical-Keyword-based Naming Scheme, Fukui Kazufumi, Todoroki Nobutoshi, Tada Harumasa, Higuchi Masahiro, Taniguchi Kenichi, IPSJ SIG Notes, 2001, 10, 71, 76, 2001 01 26 , http://ci.nii.ac.jp/naid/110002774911Summary:In file systems, hierarchical naming is generally used. We are studying another naming scheme, called hierarchical-keyword-based naming. In hierarchical-keyword-based naming, a file is named by a set of keywords and keywords are organized hierarchically. In keyword-based naming, the size of the search space will become much larger than in hierarchical naming. Therefore, it is an important issue how to manage hierarchical keywords. In this paper, we discuss data structures and algorithms to perform name resolution efficiently in hierarchical-keyword-based naming.
- Hierarchical-keyword-based Naming Scheme and File Sharing based on it, Todoroki Nobutoshi, Tada Harumasa, Higuchi Masahiro, Taniguchi Kenichi, IPSJ SIG Notes, 2000, 97, 49, 54, 2000 10 19 , http://ci.nii.ac.jp/naid/110002932860Summary:In file systems, hierarchical naming is generally used. We are studying another naming scheme, called hierarchical-keyword-based naming. In hierarchical-keyword-based naming, a file is named by a set of keywords and keywords are organized hierarchically. In this paper, we discuss file sharing in hierarchical-keyword-based naming. In the case that multiple users share files, it is inconvenient to share a global name space because file organization by users is somewhat restricted in some degree. It is more desirable for users to have their own name spaces, and integrate them for file sharing. We show hierarchical-keyword-based naming is more suitable for this purpose than usual hierarchical naming. We also describe how to implement integration of name spaces in our prototype of filename management system.
- Hierarchical-keyword-based Naming Scheme and File Sharing based on it, Todoroki Nobutoshi, Tada Harumasa, Higuchi Masahiro, Taniguchi Kenichi, Technical report of IEICE. Multimedia and virtual environment, 100, 357, 49, 54, 2000 10 12 , http://ci.nii.ac.jp/naid/110003270881Summary:In file systems, hierarchical naming is generally used. We are studying another naming scheme, called hierarchical-keyword-based naming. In hierarchical-keyword-based-naming, a file is named by set of keywords and keywords are organized hierarchically. In this paper, we discuss file sharing in hierarchical-keyword-based naming. In the case that multiple users share files, it is inconvenient to share a global name space because file organization by users is somewhat restricted in some degree. It is more desirable forusers to have their own name spaces, and integrate them for file sharing. We show hierarchical-keyword-based naming is more suitable for this purpose than usual hierarchil naming. We also describe how implemencat integration of name spaces in our prototype of filename management system.
- A Method of Generating Efficient Test Suites for Conformance Testing of EFSM Protocols, Beppu Akira, Higuchi Masahiro, Fujii Mamoru, IPSJ SIG Notes, 99, 4, 109, 114, 1999 01 21 , http://ci.nii.ac.jp/naid/110002938349Summary:In this paper, we propose the method of generating efficient test suites for conformance testing of communication protocols modeled as Finite-State Machine with Counters(FSM-C), a class of Extended Finite-State Machines (EFSM). Previously, we proposed a test suite generation method for FSM-C. The test suites can detect all single fault of the implementation, but those are not efficient, because every test case is generated for sigil test item, individually. We investigate a generating procedure of test cases which can be used for multiple test items. We also developed a test suite generating system based on the proposed method, and verified that the length of the test suites generated by the system is shorter than 20% of those generated by the previous test suite generation method for some sample protocols.
- Fault Coverage Evaluation of Test Cases Generation Method for EFSM using a Mutation System, Kohara Masaru, Higuchi Masahiro, Fujii Mamoru, IPSJ SIG Notes, 98, 8, 25, 30, 1998 01 29 , http://ci.nii.ac.jp/naid/110004062340Summary:We have proposed a test cases generation method for communication protocols modeled as Extended Finite-State Machine (EFSM). Our method can detect any single fault of protocol implementations under a restricted model called FSM-C. In this research, we evaluated fault coverage of our method and the existing methods under a general fault model. We supposed that protocols are implemented by C programs, and used a fault model based on a statistical classification. We implemented a mutation system, which generates implementations which include one fault (mutation). We examined whether the methods can detect faults in the mutations. The experiment has shown that the fault coverage of our method is superior to other methods.
- A Verification Method for Temporal Properties of Communication Protocols modeled as EFSMs, Hara Keigo, Higuchi Masahiro, Fujii Mamoru, IPSJ SIG Notes, 96, 108, 53, 58, 1996 11 14 , http://ci.nii.ac.jp/naid/110002946072Summary:In this paper, a verification method for leads-to property of communication protocols modeled as EFSMs is proposed. A leads-to property "GS(P)→GS(Q)" represents that "if a global state satisfies the property P, then the protocol eventually transits to the global states satisfying the property Q". Property P and Q are described as simultaneous inequalities using several integral parameters (called PQ-parameter). In our method, intermediate properties between P and Q are generated. Using these intermediate properties, the set of reachable global states RS is divided into RS_1, RS_2,..., and RS_n, and a leads-to reachability graph (LRG) which represents the relation between those subsets is constructed. By exploring such a LRG, "GS(P)→GS(Q)" can be shown to hold.
- An Experimental Evaluation of a Test Seaquence Generation Method for Register Operation in Communication Protocols, Proceedings of the Society Conference of IEICE, 1996, 2, 1996 09 18 , http://ci.nii.ac.jp/naid/110003337806
- A Method for Constructing Self-Stabilizing Communication Protocols modeled as 2-ECFSMs, Katakura Kenichi, Higuchi Masahiro, Fujii Mamoru, IPSJ SIG Notes, 96, 12, 13, 18, 1996 01 25 , http://ci.nii.ac.jp/naid/110002938107Summary:For implementing reliable communication systems, it is important to design communication protocols considering faults. In this paper, we propose a method in which self-stabilizing protocols are constructed based on communication protocols which are shown to be safe on the assunmption that no faults occur in 2-ECFSM model: In proposing method, protocols are extended to be able to recover from every deadlock state or unspecified reception state to a safe state by adding some action. As such a safe state, a state is chosen so that it is the closest to current state among all safe states. For such a purpose, we define a distance between two states in a protocol, and discuss some properties that hold on the notion.
- Semi-Automated Generation of Fault-Tolerance Communication Protocols in ECFSM model, Katakura Kenichi, Higuchi Masahiro, Fujii Mamoru, 51, 1, 87, 88, 1995 09 20 , http://ci.nii.ac.jp/naid/110002876731
- An implementation of invariant formula generator system for verifying ECFSM communication protocols, Hara Keigo, Sano Junko, Higuchi Masahiro, Fujii Mamoru, 51, 1, 89, 90, 1995 09 20 , http://ci.nii.ac.jp/naid/110002876733
- A Method for Generating Test Cases for a Register Assignment of Models of a Subclass of EFSM, Nakaishi Takaharu, Higuchi Masahiro, Fujii Mamoru, IPSJ SIG Notes, 95, 53, 57, 62, 1995 05 25 , http://ci.nii.ac.jp/naid/110002938250Summary:Generating test cases is significant for conformance testing of communication protocols. In this paper, we propose a method for generating test cases for communication protocols modeled as FSM with counters (FSM-C), a subclass of Extended Finite-State Machines (EFSM). FSM-C has several integral registers. Operations on registers are restricted within assignments, additions and subtractions of an integer, and comparisons of two registers. By using proposing method, it is possible to generate a set of test cases that can detect a single fault of conditons and register assignments. Lastly we illustrate our method with an example.
- Automatic Generation of Invariant Formula for Communication Protocols Modeled as ECFSMs, Higuchi Masahiro, Tamai Junko, Hara Keigo, Fujii Mamoru, IPSJ SIG Notes, 95, 53, 105, 110, 1995 05 25 , http://ci.nii.ac.jp/naid/110002938258Summary:Previously, we proposed a verification method via invariant for communication protocols modeled as ECFSMs. In the proposed method, a human verifier describes an invariant of a given protocol, and a verification system shows safety or liveness using the invariant. The tedious work on describing invariant formula is a significant shortcoming of the proposed method. This paper deal with a semiautomated derivation of invariant formula for communication protocols modeled as ECFSMs. In the method, formula holds on the states, which is reachable by synchronous communication and sending transitions, are automatically derived. We conducted an experiment on deriving disjuncts of invariant formula of a sample protocol extracted from the OSI session protocol. Among 472 disjuncts of an invariant formula, 445 disjuncts are automatically derived.
- A Method for Generating Test Cases for a Class of EFSM : Testing the Correctness of Register Assignments, Nakaishi Takaharu, Higuchi Masahiro, Fujii Mamoru, 50, 1, 163, 164, 1995 03 15 , http://ci.nii.ac.jp/naid/110002875095
- A Method for Verifying Liveness of Communication Protocols Modeled as ECFSMs, Sugawa Satoshi, Higuchi Masahiro, Fujii Mamoru, IPSJ SIG Notes, 94, 6, 231, 238, 1994 01 20 , http://ci.nii.ac.jp/naid/110002945719Summary:The authors of this paper proposed a method for verifying safety of communication protocols modeled as two ECFSMs with bilateral unbounded FIFO channels connecting them. This paper presents a method for verifying liveness of communication protocols which have been already verified to be safe by the above method. Liveness property can be formulated as Q-liveness which states "any state reachable from an initial state can reach a state which satisfies some property Q". In the proposing verification method, a set of states reachable from an initial state of a given protocol ∏ is divided into some subsets GS_1,GS_2, ・・・,GS_n. Our method constructs a directed graph DRG_<∏> whose vertex v_i(1≤i≤n) represents GS_i and whose edge from v_i to v_i expresses "∀gs ∈ GS_i∃gs' ∈ GS_i{gs' is reachable from gs}". By exploring DGR_<∏>, ∏ is showed to be Q-live. A sample protocol extracted from the data transfer phase of the OSI session protocol was verified by the proposing method.
- Verifying Liveness Properties of Communication Protocols Modeled as Extended Communicating Finite-State Machines, SUGAWA Satoshi, HIGUCHI Masahiro, FUJII Mamoru, 47, 1, 255, 256, 1993 09 27 , http://ci.nii.ac.jp/naid/110002884429
- A Method for Analyzing Communicating Finite-State Machines Using Limited Reachability Analysis, Higuchi Masahiro, Seki Hiroyuki, Kasami Tadao, IEICE technical report. Theoretical foundations of Computing, 93, 81, 53, 60, 1993 05 27 , http://ci.nii.ac.jp/naid/110003191586Summary:Communicating finite-state machines (CFSMS) are useful abstract model for specifying and verifying communication protocols.For CFSMs whose channel boundedness is not guaranteed,since the set of global states rearchable from the initial global state is potentially infinite,traditional state exploration techniques which enumerate rearchable global states cannot be used.This paper presents a class of CFSMS,called early received compatible protocols,which are analyzable using limited reachability analysis and local reachability analysis on individual protocol machines.A procedure to transform a given protocol into an equivalent ealy received compatible protocol is proposed.As an example,extension of alternating bit protocol by using the procedure to meet early received compatibility is also described.
- A Verification for OSI Session Protocol Modeled as Extended Communicating Finite Stste Machines, SANO Tetsuo, HIGUCHI Masahiro, SEKI Hiroyuki, KASAMI Tadao, 45, 1, 165, 166, 1992 09 28 , http://ci.nii.ac.jp/naid/110002889147
- A Verification Example for Communication Protocol Including Prority Services, TAMAI Junko, HIGUCHI Masahiro, SEKI Hiroyuki, KASAMI Tadao, 44, 1, 215, 216, 1992 02 24 , http://ci.nii.ac.jp/naid/110002888136