文献一覧: コンピュータソフトウェア = Computer software (雑誌)

1 0 0 0 IR CafeOBJ入門(1) : 形式手法とCafeOBJ

著者: 二木厚吉緒方和博中村正樹 Kokichi Futatsugi Kazuhiro Ogata Masaki Nakamura 北陸先端科学技術大学院大学情報科学研究科北陸先端科学技術大学院大学情報科学研究科北陸先端科学技術大学院大学情報科学研究科 Graduate School of Information Science Japan Advanced Institute of Science and Technology (JAIST) Graduate School of Information Science Japan Advanced Institute of Science and Technology (JAIST) Graduate School of Information Science Japan Advanced Institute of Science and Technology (JAIST)
出版者: 日本ソフトウェア科学会
雑誌: コンピュータソフトウェア = Computer software (ISSN:02896540)
巻号頁・発行日: vol.25, no.2, pp.1-13, 2008-04-24
参考文献数: 6
被引用文献数: 3

CafeOBJ言語システムを用いた形式手法,すなわち形式仕様の作成法と検証法,を全6回にわたり解説する.CafeOBJ言語はOBJ言語を拡張した代数仕様言語であり,振舞仕様,書換仕様,パラメータ化仕様などが記述できる最先端の形式仕様言語である.CafeOBJ言語システムは,等式を書換規則として実行することで等式推論を健全にシミュレートすることができ,対話型検証システムとして利用出来る.第1回の今回は,「待ち行列を用いる相互排除プロトコル」を例題として,言語や検証法の細部に立ち入ることなく,CafeOBJ仕様の作成と検証が全体としてどのように行われるかを説明する.第2回以降では,言語の構文と意味(第2回),等式推論と項書換システム(第3回)について説明し,証明譜を用いた簡約のみに基づくCafeOBJの検証法(第4回)を解説する.さらに,認証プロトコル(第5回)と通信プロトコル(第6回)の2つの典型的な検証例も示すことで検証の技法についても解説する.The formal method, or the method for writing and verifying formal specifications, with the CafeOBJ language system is described in a series of six tutorials. The CafeOBJ language is a most advanced formal specification language which extents the OBJ language, and behavioral, rewriting, and parameterized specifications can be written in it. The CafeOBJ language system can simulate equational reasoning by executing equations as rewrite rules, and be used as an interactive verification system. This first tutorial presents an overview of the CafeOBJ formal method by using an example of "mutual exclusion protocol with a waiting queue" without getting into details of the language and the verification technique. In the following tutorials, the language and its semantics (2nd tutorial), equational reasoning and term rewriting systems (3rd tutorial) are presented, and the CafeOBJ's verification method with proof scores which only uses reductions (4th tutorial) is explained. Furthermore, CafeOBJ's verifications of an authentication protocol (5th tutorial) and a communication protocol (6th tutorial) are also presented, and several verification techniques are explained.

2018-03-04 22:44:48
1 + 0 Twitter

https://ci.nii.ac.jp/naid/110006664762

1 0 0 0 OA あみぐるみのための3次元モデリングと製作支援インタフェース(<特集>インタラクティブシステムとソフトウェア)

著者: 五十嵐悠紀五十嵐健夫鈴木宏正 Yuki Igarashi Takeo Igarashi Hiromasa Suzuki 東京大学大学院工学系研究科東京大学大学院情報理工学系研究科:JST ERATO 東京大学大学院工学系研究科 Dept. of Engineering The University of Tokyo Dept. of Information Science and Technology The University of Tokyo:JST ERATO Dept. of Engineering The University of Tokyo
雑誌: コンピュータソフトウェア = Computer software (ISSN:02896540)
巻号頁・発行日: vol.26, no.1, pp.51-58, 2009-01-27

"あみぐるみ"は毛糸を使って作るぬいぐるみであるが,毛糸の編み方によって形状をデザインしていくため,初心者にはデザインすることが困難である.我々は3次元モデリングプロセスにインタラクティブな物理シミュレーションを組み合わせることであみぐるみを効率的にデザインできるモデラーを作成した.本システムは自動で編み目を計算してあみぐるみモデルをシミュレーション結果として提示するため,初心者にでも直感的にデザインでき,編み図も容易に得ることができる.また,初めてあみぐるみに挑戦する初心者でも製作手順を容易に理解できるようにするために,製作手順を視覚的に提示する製作支援インタフェースも備えた.あみぐるみ初心者でも容易にオリジナルなあみぐるみを作成できることを確認したので報告する.

2017-09-22 02:12:20
1 + 1 Wikipedia

http://id.nii.ac.jp/1141/00288893/

1 0 0 0 IR Monad Morphismによる局所的状態の表現

著者: 香川考司 Koji Kagawa 京都大学数理解析研究所 Research Institute for Mathematical Sciences Kyoto University.
出版者: 日本ソフトウェア科学会
雑誌: コンピュータソフトウェア = Computer software (ISSN:02896540)
巻号頁・発行日: vol.11, no.5, pp.377-386, 1994-09-16
参考文献数: 18

破壊的代入,入出力などの副作用を関数型言語で模倣するプログラムを書く際に,副作用をmonadというある種の条件を満たす型構成子として表現すると,プログラムの可読性,変更のしやすさなどが増すことがわかってきている.しかし,従来では代表的な副作用である"状態"を扱う場合に,1つの(平板な)構造しか状態として扱うことができず,関数型言語の特徴の1つである,組やリストなどの階層的データをその構造を生かして状態として扱うことは難しかった.その結果,状態を扱うプログラムをこれらのデータ型を介して部品化することができないため,あるデータ型の状態を対象として書かれたプログラムの部品を,他のデータ型を状態として持つ場合に再利用することが難しく,関数型言語にmonadを導入する動機の1つである命令的プログラムの書換え,再利用の容易性が達成されたとはいい難かった.例えば,配列を2つ以上扱いたい時に,どのように配列を1つだけ扱うプログラムの部品を再利用してプログラムを書けばいいのか,その方法がわからなかった.この論文では,階層的なデータ型の中の構成要素の"位置"をmonad morphismとして表現し,その位置にあるデータを局所的状態として扱うことにより,複合的,階層的なデータをその構造に自然な形で状態として扱う方法を提案する.その結果,プログラムの部品化を容易に行なうことができるようになる.結果としてのプログラミングのスタイルは,オブジェクト指向プログラミングを思い起こさせるものとなる.ここでは,オブジェクト指向との対応についても述べる.

2017-09-15 11:15:46
1 + 0 Twitter

https://ci.nii.ac.jp/naid/110003743830

1 0 0 0 OA 幸運な自然児 : 高橋秀俊先生を偲ぶ

著者: 近藤正夫 Masao Kondo 学習院大学
雑誌: コンピュータソフトウェア = Computer software (ISSN:02896540)
巻号頁・発行日: vol.2, no.4, pp.640-642, 1985-10-15

2017-09-04 15:51:52
1 + 0 Twitter

http://id.nii.ac.jp/1141/00286839/

1 0 0 0 OA なかよしグループ問題と属性文法への応用

著者: 山下義行佐々政孝中田育男 Yoshiyuki Yamashita Masataka Sassa Ikuo Nakata 筑波大学電子情報工学系筑波大学電子情報工学系筑波大学電子情報工学系
雑誌: コンピュータソフトウェア = Computer software (ISSN:02896540)
巻号頁・発行日: vol.4, no.3, pp.212-224, 1987-07-15

「なかよしグループ問題」は,ある条件下での集合の彩色問題を一般化し,より親しみやすい表現に直したものである.この問題ではなかよしグループの子供達に最適な色のキャンディを配ることを考えるが,配色に関する制約条件,局所的な最適条件および大局的な最適条件が絡みあい,必ずしも簡単には解けない.そこで,なかよしグループの中からキーとなる子供達を見つけ出し,その子らについて彩色問題を解くだけで総ての子供達への配色が決まる,という一般的な解法を提案する.応用として,ECLR属性文法に基づくコンパイラ生成系Rieの属性スタック自動割り当てプログラムを作成し,PL/0,Pascalサブセットコンパイラについて最適な割り当てを行った.

2017-07-24 19:30:17
1 + 1 Twitter

http://id.nii.ac.jp/1141/00286956/

1 0 0 0 IR 再利用と再発明(特集・新世紀フォーラム)

著者: 藤波順久 Nobuhisa Fujinami ソニー(株)インフォメーション&ネットワーク研究所 Information & Network Technologies Laboratories Sony Corporation
出版者: Japan Society for Software Science and Technology
雑誌: コンピュータソフトウェア = Computer software (ISSN:02896540)
巻号頁・発行日: vol.17, no.1, pp.29-31, 2000-01-17

2017-07-24 17:52:07
1 + 0 Twitter

1 0 0 0 OA 米田信夫先生を悼む

著者: 筧捷彦早稲田大学
雑誌: コンピュータソフトウェア = Computer software (ISSN:02896540)
巻号頁・発行日: vol.13, no.4, pp.355, 1996-07-15

2017-06-25 23:20:51
1 + 0 Twitter

http://id.nii.ac.jp/1141/00287730/

2014-10-23 00:42:07
1 + 0 Twitter

https://ci.nii.ac.jp/naid/110003743879

1 0 0 0 IR コネクショニズムの挑戦に古典的計算主義はどうこたえるか

著者: 徃住彰文 Akifumi Tokosumi 聖心女子大学文学部心理学科
雑誌: コンピュータソフトウェア = Computer software (ISSN:02896540)
巻号頁・発行日: vol.5, no.3, pp.273-279, 1988-07-15

1988年12月の日本認知科学シンポジウムにおける,カナダ,ウェスタン・オンタリオ大ゼノン・ピリシン教授の講演要約を中心に,認知を記号表現の上での計算とみなす古典的計算主義の立場からのコネクショニズム批判の現況を紹介した.

2012-07-22 18:15:58
1 + 2 Wikipedia

https://ci.nii.ac.jp/naid/110003743502

1 0 0 0 IR 意味表現の階層に基づく自然言語生成システム (<特集>自然言語処理における統合)

著者: 池田光生 Teruo Ikeda (財)新世代コンピュータ技術開発機構
出版者: 日本ソフトウェア科学会
雑誌: コンピュータソフトウェア = Computer software (ISSN:02896540)
巻号頁・発行日: vol.8, no.6, pp.536-545, 1991-11-15

多くの生成システムでは,プランニング部と表層文生成部との間で中間構造を介して情報の伝達を行う.生成処理が多様化するにつれて複雑になる中間構造を,簡潔に記述するために,五つの階層からなる意味表現を導入した.各階層は文の統語的な階層構造を反映したものであり,統語的な制約を自然な形で意味の階層の中に埋め込むことにより,統語的な制約と意味的,文脈的な制約を統合している.意味表現の階層を用いることにより,多様な従属節の接続表現の違いや提題の「は」の役割を,記述する階層の違いとして自然に明示することができる.

2011-07-21 02:40:53
1 はてなブックマーク

https://ci.nii.ac.jp/naid/110003743651

1 0 0 0 IR リクエスト待機間隔を考慮したウェブサーバのkeep-alive時間の自動設定

著者: 杉木章義河野健二岩崎英哉 Akiyoshi Sugiki Kenji Kono Hideya Iwasaki 電気通信大学大学院電気通信学研究科情報工学専攻慶應義塾大学理工学部情報工学科電気通信大学電気通信学部情報工学科 Department of Computer Science Graduate School of Electro-Communications The University of Electro-Communications Department of Information and Computer Science Keio University Department of Computer Science The University of Electro-Communications
出版者: Japan Society for Software Science and Technology
雑誌: コンピュータソフトウェア = Computer software (ISSN:02896540)
巻号頁・発行日: vol.24, no.2, pp.68-78, 2007-04-24
参考文献数: 27
被引用文献数: 7

インターネットサーバの手動による性能パラメータ調整は,多くの経験や時間を必要とし,管理コストの増大を招くことが知られている.ウェブサーバの主要な性能パラメータであるkeep-alive時間は,適切に設定しない場合,サーバのスループットや応答性を低下させることがある.本論文では,ウェブサーバのkeep-alive時間の自動設定機構を提案する.本機構は管理者の介入を必要とせず,手動設定で求めた値に近いkeep-alive時間に自動設定する.本機構はリクエスト待機間隔を監視しながら,データを送受信していない接続を切断し,データを頻繁に送受信している多くのクライアントからの接続を保つようにkeep-alive時間を設定する.本機構をApacheウェブサーバを対象としたライブラリとして実装し,実験を行った.その結果,異なる2つの負荷に対して,それぞれkeep-alive時間を自動的に設定し,サーバの性能を適切に維持することを確認した.Manual parameter-tuning of Internet servers causes high administrative costs because it requires administrator's expertise and huge amounts of time. The keep-alive parameter, which is one of major parameters in web servers, may cause severe degradation if it is not set properly. In this paper, we present an automatic tuning technique of the keep-alive parameter. Our mechanism adjusts the parameter without administrator's intervention so as to maintain active connections between clients and a server while closing inactive connections by observing request-waiting intervals. We implemented a prototype for Apache web server. Experimental results show that our prototype automatically adjusted the parameter and successfully yielded the nearly optimal server performance on two different workloads.

2009-10-29 01:02:18
1 はてなブックマーク

1 0 0 0 IR Bluetoothによる位置検出

著者: 勝野恭治相原達水谷晶彦玉川憲 Yasuharu Katsuno Toru Aihara Akihiko Mizutani Ken Tamagawa 日本アイ・ビー・エム株式会社東京基礎研究所日本アイ・ビー・エム株式会社東京基礎研究所日本アイ・ビー・エム株式会社東京基礎研究所日本アイ・ビー・エム株式会社東京基礎研究所 IBM Research Tokyo Research Laboratory IBM Research Tokyo Research Laboratory IBM Research Tokyo Research Laboratory IBM Research Tokyo Research Laboratory
出版者: 日本ソフトウェア科学会
雑誌: コンピュータソフトウェア = Computer software (ISSN:02896540)
巻号頁・発行日: vol.20, no.5, pp.492-496, 2003-09-25
参考文献数: 7

本論文では,様々な携帯デバイスに搭載されている短距離無線通信技術, Bluetoothを用いた距離検出方法を提案する.無線通信として搭載されているBluetoothでデバイス間の距離を検出できれば,デバイスの位置が相対距離で検出できる.そのため,位置情報を利用したサービスをBluetooth搭載デバイスに提供することが可能となる.さらに本方法を用いたアプリケーション例として, Bluetooth搭載腕時計型コンピュータ, WatchpPad 1.5を身につけたユーザーとの相対距離に応じて提供するコンテンツを変えるインフォメーションキオスクシステムを試作し,本方法の有効性を確かめる.