Search

Your search keyword '"Kishi, Tomoji"' showing total 37 results
Start Over Author "Kishi, Tomoji"
37 results on '"Kishi, Tomoji"'

1. Model-Checking in the Loop Model-Based Testing for Automotive Operating Systems

Author

Aoki, Toshiaki, Hata, Aritoshi, Kanamori, Kazusato, Tanaka, Satoshi, Kawamoto, Yuta, Tanase, Yasuhiro, Imai, Masumi, Shigemitsu, Fumiya, Gondo, Masaki, and Kishi, Tomoji

Subjects
Computer Science - Software Engineering
Abstract

While vehicles have primarily been controlled through mechanical means in years past, an increasing number of embedded control systems are being installed and used, keeping pace with advances in electronic control technology and performance. Automotive systems consist of multiple components developed by a range of vendors. To accelerate developments in embedded control systems, industrial standards such as AUTOSAR are being defined for automotive systems, including the design of operating system and middleware technologies. Crucial to ensuring the safety of automotive systems, the operating system is foundational software on which many automotive applications are executed. In this paper, we propose an integrated model-based method for verifying automotive operating systems; our method is called Model-Checking in the Loop Model-Based Testing (MCIL-MBT). In MCIL-MBT, we create a model that formalizes specifications of automotive operating systems and verifies the specifications via model-checking. Next, we conduct model-based testing with the verified model to ensure that a specific operating system implementation conforms to the model. These verification and testing stages are iterated over until no flaws are detected. Our method has already been introduced to an automotive system supplier and an operating system vendor. Through our approach, we successfully identified flaws that were not detected by conventional review and testing methods.

Published
2023

6. Design Verification for Product Line Development

Author

Kishi, Tomoji, Noda, Natsuko, Katayama, Takuya, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Dough, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Obbink, Henk, editor, and Pohl, Klaus, editor

Published
2005
Full Text
View/download PDF

12. 2nd Workshop on Scalable Modeling Techniques for Software Product Lines (SCALE 2010)

Author

Baba, Muhammad Ali, Cohen, Sholom, Kang, Kyo C., Kishi, Tomoji, van der Linden, Frank, Noda, Natsuko, Pohl, Klaus, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Bosch, Jan, editor, and Lee, Jaejoon, editor

Published
2010
Full Text
View/download PDF

17. Combined Model Checking and Testing Create Confidence in Correctness of Commercial Automotive Operating System

Author

Aoki, Toshiaki, Satoh, Makoto, Tani, Mitsuhiro, Yatake, Kenro, and Kishi, Tomoji

Subjects
automotive operating systems, test case generation, model checking, testing, design verification
Abstract

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., リサーチレポート（北陸先端科学技術大学院大学先端科学技術研究科情報科学系）

Published
2016

21. Report on Winter Workshop 2012 in Biwako

Author

Maruyama, Katsuhisa, Omori, Takayuki, Igaki, Hiroshi, Nakamura, Masahide, Fushida, Kyohei, Tsunoda, Masateru, Kazato, Hiroshi, Okada, Joji, Okano, Kozo, Sakamoto, Kazunori, Motohashi, Masanari, Kishi, Tomoji, Noda, Natsuko, Kobayashi, Takashi, and Hayashi, Shinpei

Abstract

2012 年 1 月 19 日， 20 日の 2 日間に，琵琶湖コンファレンスセンター （滋賀県彦根市） にて開催したウィンターワークショップ 2012・イン・琵琶湖 (WW2012) の概要について報告する．, This paper reports on “Winter Workshop 2012 in Biwako(WW2012)”, which was held at Biwako Conference Center in Hikone, Shiga from January 19 through 20, 2012.

Published
2012

23. Optimization of Product Instantiation using Integer Programming

Author

van den Broek, P.M., Botterweck, Goetz, Jarzabek, Stan, and Kishi, Tomoji

Subjects
EWI-18086, SE-Q: Quality Modelling and Verification, METIS-270884, IR-73470
Abstract

We show that Integer Programming (IP) can be used as an optimization technique for the instantiation of products of feature models. This is done by showing that the constraints of feature models can be written in linear form. As particular IP technique, we use Gomory cutting planes. We have applied this technique to a test suite of feature models from the literature, and found that the Gomory cutting planes can be used to improve the feature models. We discuss a number of applications: analysis of feature models, resolving configuration errors and optimization of product instantiation.

Published
2010

34. Design Verification for Product Line Development.

Author

Obbink, Henk, Pohl, Klaus, Kishi, Tomoji, Noda, Natsuko, and Katayama, Takuya

Abstract

Our society is becoming increasingly dependent on embedded software, and its reliability becomes more and more important. Although we can utilize powerful scientific methods such as model checking techniques to develop reliable embedded software, it is expensive to apply these methods to consumer embedded software development. In this paper, we propose an application of model checking techniques for design verification in product line development (PLD). We introduce reusable verification models in which we define variation points, and we show how to define traceability among feature models, design models and verification models. The reuse of verification models in PLD not only enables the systematic design verification of each product but also reduces the cost of applying model checking techniques. [ABSTRACT FROM AUTHOR]

Published
2005
Full Text
View/download PDF

37. Feature Petri Nets

Author

Muschevici, R., Clarke, D., José Proença, Botterweck, Goetz, Jarzabek, Stan, Kishi, Tomoji, Lee, Jaejoon, and Livengood, Steve

Subjects
Petri Nets, Software Product Lines
Abstract

In software product line (SPL) engineering, formal modelling and verification are critical for managing the inherent complexity of systems with a high degree of variability. The number of products in an SPL can be exponential in the number of features. Therefore, the challenge when modelling SPL lies in analysing and verifying large, complex models efficiently, in order to ensure that all products behave correctly. The choice of a system modelling formalism that is both expressive and well-established is therefore crucial. In this paper we propose two lightweight extensions to Petri nets: Feature Petri Nets provide a framework for modelling and verifying software product lines; and Dynamic Feature Petri Nets provide additional support for modelling dynamic software product lines. ispartof: Proceedings of the 14th International Software Product Line Conference (SPLC 2010) vol:2 pages:99-106 ispartof: Software Product Lines Conference edition:14 location:Jeju, South Korea date:13-17 September 2010 nrpages: 99-106 status: published

Published
2010

Catalog

Books, media, physical & digital resources
See catalog results