著者

真壁 徹 宇多 仁

出版者

北陸先端科学技術大学院大学先端科学技術研究科情報科学系

雑誌

Research report (School of Information Science, Graduate School of Advanced Science and Technology, Japan Advanced Institute of Science and Technology) (ISSN:09187553)

巻号頁・発行日

vol.IS-RR-2020-001, pp.1-13, 2020-07-28

---

リサーチレポート(北陸先端科学技術大学院大学先端科学技術研究科情報科学系)

著者

Hayashibara Naohiro Defago Xavier Yared Rami Katayama Takuya

出版者

北陸先端科学技術大学院大学情報科学研究科

雑誌

Research report (School of Information Science, Japan Advanced Institute of Science and Technology) (ISSN:09187553)

巻号頁・発行日

vol.IS-RR-2004-010, pp.1-15, 2004-05-10

---

Detecting 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 is the difficulty to satisfy several application requirements simultaneously when using classical failure detectors. 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 boolean 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 φ failure detector. The particularity of the φ 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 φ failure detector over an intercontinental communication link during several days. Our experimental results show that our φ failure detector performs equally well as other known adaptive failure detection mechanisms, with an improved flexibility.

著者

Beuran Razvan Chinen Ken-ichi Tan Yasuo Shinoda Yoichi

出版者

北陸先端科学技術大学院大学先端科学技術研究科情報科学系

雑誌

Research report (School of Information Science, Graduate School of Advanced Science and Technology, Japan Advanced Institute of Science and Technology) (ISSN:09187553)

巻号頁・発行日

vol.IS-RR-2016-003, pp.1-16, 2016-10-14

---

Effective cybersecurity education and training are important for preparing current and future IT professionals to properly and swiftly deal withreal-life security incidents. In this paper we use the main cybersecurity training programs in Japan as a detailed case study for analyzing the best practices and methodologies in the field of cybersecurity education and training. Based on this analysis and our first-hand experience with some of the said training programs, we then define the requirements that must be met in order to ensure effective cybersecurity education and training.Finally, we discuss our research and development endeavor towards creating a framework that meets these requirements, so as to facilitate effectiveeducation and training in cybersecurity.

著者

Aoki Toshiaki Satoh Makoto Tani Mitsuhiro Yatake Kenro Kishi Tomoji

出版者

北陸先端科学技術大学院大学先端科学技術研究科情報科学系

雑誌

Research report (School of Information Science, Graduate School of Advanced Science and Technology, Japan Advanced Institute of Science and Technology) (ISSN:09187553)

巻号頁・発行日

vol.IS-RR-2016-002, pp.1-11, 2016-05-23

---

The safety and reliability of automotive systems are becoming a big concern in our daily life. Recently, a functional safety standard which specializes in automotive systems has been proposed by the ISO. In addition, electrical throttle systems have been inspected by NHTSA and NASA due to the unintended acceleration problems of Toyota’s cars. In light of such recent circumstances, we are researching practical applications of formal methods to ensure the high quality of automotive operating systems. An operating system which we focus on is the one conforming to the OSEK/VDX standard. This paper shows a case study where model checking is applied to a commercial automotive operating system. In this case study, the model checking is combined with testing in order to efficiently and effectively verify it. As a result, we acquired the confidence that the quality of the operating system is very high.

著者

Do Ngoc Thi Bich Ogawa Mizuhito

出版者

北陸先端科学技術大学院大学情報科学研究科

雑誌

Research report (School of Information Science, Japan Advanced Institute of Science and Technology) (ISSN:09187553)

巻号頁・発行日

vol.IS-RR-2010-004, pp.1-27, 2010-06-21

---

This paper proposes a technique for automaticdetection of overflow and roundoff errors, causedby the floating-point number to fixed-point number conversion. First, a new range representation, “extended affine interval”, is proposed to overapproximate overflow and roundoff errors. Second, the overflow and roundoff error analysis problem is encoded as a weighted model checking, which is implemented as a static analyzer CANA. Last, we propose a new testing refinement loop, called “counterexample-guided narrowing”, by combining the static analysis and testing. They arecomposed and implemented in a prototype tool, CANAT, in which analysis results are used not only for possible roundoff error detection, but also for finding dominant error factors in input parameters. To avoid widening, currently we focus on programs with bounded loops and arrays with fixed length, which typically appear in encoder/decoder reference algorithms. Experimental results on small programs show that the extended affine interval is much more precise than classical interval, andthe counterexample-guided narrowing approach outperforms the random testing technique.

著者

池田 克則 落水 浩一郎

出版者

北陸先端科学技術大学院大学情報科学研究科

雑誌

Research report (School of Information Science, Japan Advanced Institute of Science and Technology) (ISSN:09187553)

巻号頁・発行日

vol.IS-RR-96-0010S, pp.1-72, 1996-03-18

---

本論文では、PCTE(Portable Common Tool Environment)を用いて、商用CASEツールのデータを統合する手段を論じたものである。様々な統合技術の調査及び開発を紹介しつつ、その結果をStP/OMTとObjectCenterの統合にまとめる。上流工程と下流工程のCASEツールをデータ統合することにより、作業の連続性の保証と変更の波及の追跡が容易に分かることが期待される。本論文ではそれを交換するためのスキーマ例の結果も示す。さらに、このツールを用いて実際のソフトウェアの開発を行ない、それに基づいて統合ツールの問題点を分析しつつ、ツール統合のありかたについて提案する。