著者

吉岡 信和 田辺 良則 田原 康之 長谷川 哲夫 磯部 祥尚

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.31, no.4, pp.4_40-4_65, 2014-10-24 (Released:2014-12-24)

---

機器の高速化やネットワークの発展に伴い,多数の機器やコンポーネントを連携させ,高度な機能を提供する並行分散システムが一般的になってきている.そのようなシステムでは,振舞いの可能性が膨大であり,従来のレビューやシミュレーションで設計の振舞いの正しさを保証することは困難である.それに対して,網羅的にかつ自動的に振舞いに関する性質を調べるモデル検査技術が注目されている.本稿では,モデル検査技術の背景と5つの代表的なモデル検査ツールを紹介し,その応用事例や最新の研究動向を解説する.

著者

池内 了 杉山 直 海部 宣男 土居 守 福島 登志夫 長谷川 哲夫

出版者

名古屋大学

雑誌

基盤研究(C)

巻号頁・発行日

2002

---

アジア・太平洋地域(オセアニア、南北アメリカも含む)における天文学研究は、多くの先進的観測装置を有する国から観測装置が未整備な国まで、さまざまな研究環境条件にある。そこで、国際天文学連合(IAU)が主催して、これらの諸国の天文学研究者が一堂に集まり、最前線の研究成果を交流しつつ、若手研究者の育成、共同研究の推進と相互援助、天文学普及のための活動、などについて情報交換を行う「IAUアジア・太平洋地区会議(略称APRM)」を開催してきた。本研究課題は、2002年7月2日から5日まで東京の一橋記念講堂で開催された、第8回APRMの準備費用・会議運営経費・報告集発行経費を賄うことによって会議の成功に寄与したものである。会議には、総計462人が参加し、うち148人は23カ国からの外国人研究者であった。会議は、全体会議行われた(1)大型観測装置、(2)大規模サーベイ、(3)太陽系外惑星、(4)天文学教育の4つのセッションと、(5)星・惑星系形成、(6)星・太陽活動、(7)高エネルギー天文学、(8)活動的銀河核、(9)重カレンズ、(10)系外銀河・宇宙論の6つのセッションが分科会で行われ、約30の招待講演、約100の口頭発表、約320のポスター発表があった。加えて、(11)情報交換のためのネットワーク形成と研究雑誌の発行、(12)今後の地域集会の予定、の2つのビジネス・セッションを持ち、アジア・太平洋地域における天文学研究のよりいっそうの発展のための討論を行った。会議の報告集として、全体会議については太平洋天文学会(ASP)の国際会議録シリーズ、分科会およびポスター論文は日本天文学会(ASJ)の国際会議録として出版した。なお、最終日の翌日の6日には4つのサテライト集会が持たれ、これにも多数の研究者が参加した。

著者

長谷川 哲夫

出版者

東洋大学日本文学文化学会

雑誌

日本文学文化 = Japanese Literature and Culture (ISSN:13468723)

巻号頁・発行日

no.10, pp.43-52, 2010

著者

坪井 俊 山本 智 蓑輪 眞 西原 寛 雨宮 昭南 三谷 啓志 松本 良 江崎 雄治 朝倉 清高 長尾 敬介 長谷川 哲夫

出版者

東京大学大学院理学系研究科・理学部

雑誌

東京大学大学院理学系研究科・理学部廣報

巻号頁・発行日

vol.29, no.4, pp.24-36, 1998-03

---

カラビ不変量とオイラー類/サブミリ波望遠鏡をつくる/太陽アクシオンの直接検出実験/一次元レドックス共役分子、オリゴフェロセニレンの物性/動物の発生と左右非相称性/光回復酵素:生きながらえるべきか、死すべきか/御前崎沖南海トラフのガスハイドレート/人口「還流移動」発生率のエスティメーション/異方性表面を用いた表面原子配列制御/宇宙線生成希ガスからみた火星隕石の歴史/天の川銀河の地図をつくる

著者

青木 翼 長谷川 哲夫 宮本 博暢 渡邊 竜明

出版者

一般社団法人情報処理学会

雑誌

情報処理学会研究報告ソフトウェア工学(SE) (ISSN:09196072)

巻号頁・発行日

vol.2008, no.29, pp.203-210, 2008-03-18

被引用文献数

1

---

モデル検査によりソフトウェア設計の品質を向上させることが注目されている.一方,モデル検査を開発に適用するノウハウはまだ不足している.本論文ではモデル検査をソフトウェア開発に適用させるためのガイドラインについて報告をする.このガイドラインではモデル検査を実施する目的と効果,モデル検査が適用できる箇所,モデルや検証式を作成する手順,モデルや検証式の記述テクニックの4点について説明を行っている.While improvement of the quality of software design using model checking is required, the current know-how pertaining to the application of model checking is insufficient. This paper describes the guideline for model checking in UPPAAL, which consists of 4 sections explaining the objectives and outcomes of model checking, target documentation, process, techniques of models and verification expressions building.

著者

坪井 俊 山本 智 蓑輪 眞 西原 寛 雨宮 昭南 三谷 啓志 松本 良 江崎 雄治 朝倉 清高 長尾 敬介 長谷川 哲夫

出版者

東京大学大学院理学系研究科・理学部

雑誌

東京大学大学院理学系研究科・理学部廣報

巻号頁・発行日

vol.29, no.4, pp.24-36, 1998-03

---

カラビ不変量とオイラー類/サブミリ波望遠鏡をつくる/太陽アクシオンの直接検出実験/一次元レドックス共役分子、オリゴフェロセニレンの物性/動物の発生と左右非相称性/光回復酵素:生きながらえるべきか、死すべきか/御前崎沖南海トラフのガスハイドレート/人口「還流移動」発生率のエスティメーション/異方性表面を用いた表面原子配列制御/宇宙線生成希ガスからみた火星隕石の歴史/天の川銀河の地図をつくる