情報工学工房「Coqで学ぶ計算機ソフトウェアの基礎」授業紹介(2020/10/11)

電気通信大学1年の伊藤です。情報工学工房の今年のコースの1つ、「Coqで学ぶ計算機ソフトウェアの基礎」の紹介をします。

授業内容を簡単に説明すると、毎回宿題として教科書を読み、証明の問題を解いてきて、解いてきた証明について、授業中に解説などをする、と言った感じです。

この授業の大きな特徴は、証明に「Coq」を使うことです。Coqというのは、証明が正しいかどうかを検証してくれるツールです。証明というと日本語や英語などの自然言語で書くのが普通ですが、Coqを使った証明では、プログラミング言語を使います。

証明の内容は、基本的な自然数の性質やリスト(配列)の性質を証明したり、とても簡単なプログラミング言語を定義してその性質を証明をしたり、アルゴリズムの正しさ(思った通りの振る舞いをするか)を確かめたり、といった感じです。教科書で扱うものはどれも、世の中で実際に扱われている対象を簡易化したものですが、演習問題は難しく、私は結構苦戦しています。

上の画像は、実際に証明を組み立てている画面です。鳩の巣原理を証明しようとしています(鳩の巣原理を知らない場合は調べて下さい)。まだ証明できていません。演習問題の答えをネット上の検索エンジンで検索できる場所に上げないで下さいと教科書に書いてあるので、一応まだ解けていない問題を選んでみました。こんなことも証明できるのかと驚いた問題の1つです。まだ証明できていませんが…

まだまだ授業は続くので、引き続き腕を磨いていきたいと思います。

MICS杯

9月5日〜25日の期間に、MI/CSコースの学生を対象にFPGAを使ったゲーム大会(MICS杯)を開催しました。MICS杯ではゲームを設計する設計部門、作ったゲームをプレイする競技部門があり、参加者はそれぞれの部門で競い合いました。

MICS杯では前期のJ1実験で使用したリモートで操作可能なFPGAボードを使用しました。このFPGAボードではGUIアプリケーションを使ってFPGAボード上のスイッチを操作したり、カメラからオシロスコープの波形を確認したりすることができます。

※リモート操作可能なFPGAボードについてはこちらの記事でも紹介されています。

設計部門は5日から23日まで行われました。最終的に3つのゲームがエントリーしました。

・Light out:全てのランプを消すようにスイッチを押すゲーム

・FPGAマインスイーパー:周辺の地雷の数から地雷の入ってないマスを見つけるゲーム

・洞窟Run:岩(上の波形)を避けながら洞窟を走るゲーム

競技部門では24日に予選が、25日に決勝戦が行われました。表彰式では藤井雄大さんが優勝、ブシャダさんが敢闘賞、桃太さんが設計部門賞で表彰されました。

MICS杯は公式Twitterアカウントもあります。Twitterでは設計部門で投稿されたゲームの動画での紹介などをしています。是非ご覧ください!!

https://twitter.com/MICScup_uec











※ここから先はMICS杯の裏話

MICS杯は成見研主催で開催されました。

成見研究室では毎年9月に夏の合宿を行っています。夏合宿では昼間に旅行先で遊んだり、夜にB4の学生の卒研中間発表の練習をしたりします。しかし今年は新型コロナウイルス感染症の影響で合宿は中止となりました。そこで合宿の代わりとなったイベントがMICS杯だったのです。

予選・決勝を行った24日、25日の午前中は研究室で密を避けながら発表練習をしました。午後はご飯を食べにお出かけをして、夕方からMICS杯の準備、開催をしました。

25日のお昼は調布飛行場に隣接するプロペラカフェに行きました。

窓から見える滑走路

プロペラカフェのハンバーガー

VRフライトシミュレータを体験する成見先生

前期CED TAを振り返って。CEDのオンラインでの取り組みのまとめ

2020年度 I類(情報系)計算機室 (CED) のTAの青見です。本日は、CEDにおける今年度前期のTA業務について軽く振り返ってみようと思います。

本記事執筆時点でのCEDのHP (https://www.ced.cei.uec.ac.jp/) の様子

多くのI類の学生の皆さんは御存知だと思いますが、主にI類・I専攻の学生向けの計算機室として、西9号館に”CED”が設置されています。私たちCED TAは、主に計算機室の閉館作業や、現地での利用者の質問対応等を行う……予定でしたが、昨今の新型コロナウイルスの影響もあり、今学期はCEDのオンラインでの取り組みの補助業務を行っておりました。

今学期より始めた取り組みのうちの一つとして、”Zoomオフィスアワー”があります。これは、決まった時間にCED TAがZoomのミーティングルームを開放しておき、時間内の好きなタイミングでCEDの利用方法や、オンライン講義のための設定補助をしていました。

CEDのHP (https://www.ced.cei.uec.ac.jp/) 最下部の”Zoomオフィスアワー”

私自身も、本URLを見つけていらっしゃった方や、事前にCED宛にメールを頂いた方を中心に何人かの補助をさせていただきました。お役に立っていれば幸いです。

また、普段リモート接続されなかった学生の方を中心に、CEDと手元のPCとのファイルの送受信の方法について問い合わせをいただくことがありました。これに合わせ、scpsftpといったコマンドの使い方や、MobaXtermを用いたGUIによるSFTPのファイル送受信方法の資料を作製し、CED HPに掲載していただきました。

CEDのHP (https://www.ced.cei.uec.ac.jp/) 中段部「お願い」に掲載していただきました!

簡易的な資料ではありますが、こちらの資料を通して「意外と簡単だな」と思って、積極的に利用していただけると幸いです。後期になるとCEDの利用者も増えると思いますが、わからない方はぜひ一度目を通してみてください。

さらに今年度CEDでは、CEDのGUI環境を実行するためにVNCの利用方法をHP上に掲載しています。こちらのVNC Viewerの設定方法も調査し、記載させていただきました。情報数理工学/コンピュータサイエンス実験第一のJ1実験では、CEDの計算機にインストールされている回路設計のためのアプリケーションをGUI上で動作させる必要があり、非常に多くの人に利用していただきました。私たちも、実際にJ1実験の時間に実験のZoomに参加し、導入の補助を行いました。今学期のJ1実験に関しては下の記事を御覧ください。

後期はI類1年生の利用も増え、今までCEDを使ったことのない利用者が増えることが予想されます。そういった学生が使いやすいように、出来る限りのサポートをさせていただきたいです。よろしくお願いいたします。

情報工学工房ダンボールコミュニケーションロボットチーム2020前期活動紹介(2020/8/14)

こんにちは!Ⅰ類(情報系)1年の江連と大住です。ここでは情報工学工房について紹介します。
電気通信大学にはⅠ類、Ⅱ類、Ⅲ類の3つの類があり、Ⅰ類では情報に関すること(AI、VRなどもあります)を学ぶことができます。そしてⅠ類を目指そうという人に特におすすめなのがこの情報工学工房です。情報工学工房とは、ロボットを動かしたり、プログラミングしたり、AIを使って小説を書いたり、、、など(詳しくはホームページへ)好きなテーマを選んで1年間開発する授業らしくない授業です。大学では何十人もの学生が一斉に授業を受けることがほとんどですが、この情報工学工房では、少人数で自分の興味があることを学ぶことができます。

昨年の活動はこちら 

ダンボールコミュニケーションロボットチームはロボットを組み立て、各自が命令を書き込んで自己紹介をさせました。ロボットは「センサー、知能・制御系、駆動系の3つの要素技術を有する知能化した機会システム」(出典:総務省 コミュニケーションロボットとは)と定義されており、すでにボタンを押すとパターンに従ってロボットに喋らせることができています。また、駆動系として首が可愛くフリフリ動きます。
このロボットには自分でセンサーを追加したり、プログラミングでより高度な制御を目指したりと、可能性が無限大にあります。現在は自分がやりたいサービスを実現するために何をするべきなのか、イメージを膨らませています。

前期の工房は、Zoomを用いたオンラインのみの活動になりましたが、OBやエンジニアの山口さん、庄野先生のサポートもあり、ダンボールコミュニケーションロボットに関わる技術を学べました。後期には、実際にそれぞれがダンボールコミュニケーションロボットを開発し、様々なサービスを検討したいと思います!

J1実験:論理回路(オンライン実験)の紹介(2020/8/14)

こんにちは!I類(情報系)計算機室管理者の島崎です。本日は、I類(情報系)3年次の情報数理工学実験第一・コンピュータサイエンス実験第一のJ1課題(論理回路)についてご紹介します。
※昨年の投稿はこちら

電通大は現在、新型コロナウィルス感染症の影響で、前期授業は原則、オンラインで実施しています。
その中で、実験もオンラインで実施することになりましたので、I類(情報系)成見先生、赤池先生と遠隔で実験が可能なリモートコントロールアプリとFPGAボードを開発しました。

従来は、学生がFPGAボードやオシロスコープを操作して実験を行うのですが、オンラインだと操作ができません。
そこで、下記のようにFPGAボードとオシロスコープを遠隔で操作するための基板を新たに開発し、Arduinoを用いて操作する仕組みを25台分用意しました。具体的には、下記のようになっています。

開発には、実際にJ1実験を受講したことがある大学院生のTAも協力してもらい、CAD化や半田付けを担当してもらいました。

実験は、7/8 から 8/5 に3つの組に分けて、Zoomを用いて実施しました。学生は、遠隔での実験に苦労しており、頑張ってレポート書いています。今後、遠隔での実験方法を検証するために、実施したアンケートとログデータを分析して論文にまとめる予定です。今後、オンラインでの実験や演習についてI類(情報系)の様子を学生が発信してくれる予定ですので楽しみにしてください!※学生と教員と協力して、なるべくI類(情報系)の様子が伝わるよう努力いたします、、。

FPGA&Unity班2020前期中間発表(2020/7/7)

先日の情報工学工房の中間発表の中から、いくつか気になった作品を紹介します。

【Unity班】

・振り子の物理シミュレーション

・的当てゲーム

・弾幕ゲーム

また、中間発表ということもあり、以下の例のようなものを途中まで作った・これから作ってみたいという発表も多かったです。

・VRタワーディフェンスゲーム

・ブロック崩し

・FPS(シューティングゲーム)

・2人用VR協力アクションゲーム

・音声認識でキャラクターと触れ合う

【FPGA班】

FPGA班についても、前年度と異なったチャレンジをしたいなどの理由から以下のようなものを作ってみたいという発表がありました。

・ブラシレスモーターのベクトル制御

・FPGAボードの自炊

・テトリス

・自作CPU

・ファミコンを再現

・FPGAでドローンを飛ばす

・TPUを作りたい

今回は中間発表ということもあり、まだ未完成だったりこれからやりたいことがある人が多い印象でした。最終発表までにどのような作品が仕上がっていくのか楽しみです。

寺崎

VR授業@コンピュータグラフィックス

MICSで開講されている、成見先生の担当するコンピュータグラフィックスの授業では今回、UnityとKinectを利用したVR授業の試作に取り組みました。その様子と、簡単な仕組みについて紹介します。

普段のコンピュータグラフィックスの授業では三次元CGの基本的な要素技術やOpenGLのAPIを用いたプログラムの作成技術を学びます。

VR授業には、同じく成見先生が指導する学食テレビの活動の一環として開発された、電通大を舞台にしたモバイルアプリ「U Explore Canvas」(UExC)から接続します(iPhone用Android用)。

実際のアプリ上では、以下の動画のような様子になっています(音声付き動画)。

Kinectで黒板を撮影しながら、人体の検出を行い先生を消去しています。また、骨格を取得してバーチャルなキャラクターが先生と同じ動きをしています。さらに、上の動画のリンク先で音声を確認するとわかりますが、ボイスチェンジャーによって先生の声が女声に変換されています。

また、土台となっているUExCはゲームアプリなので、もちろん周囲をゲームのように動き回ることも可能です。以下の動画では黒板の周りを歩き回ったり視野を回転しています。

このVR授業には現在学内ネットワークからでないと接続できないようになっているので、自宅からアプリ内で授業を受ける、という訳にはまだいきませんが、未来の新たな授業のあり方を感じさせてくれるのではないでしょうか。

FPGA&Unity班2019後期最終発表(2020/2/7)

Unity班のTAの寺崎です。

今日は情報工学工房の後期最終発表があったので、その様子をご紹介します。

・FPGA班

FPGA班の発表では、Twitterに学内掲示板の写真が投稿された際に自動でリツイートする情報収集用botを作成した学生の発表や、FPGAボードを自作した学生の発表などが行われました。

・Unity班

Unity班の発表では、マルチVRプラットフォームを自作した学生の発表や、脱出ゲームを作成した学生の発表、スライムとフリスビーで交流できるゲームを作成した学生の発表などが行われました。

マルチVRプラットフォームを作成した学生によると、現状作成したシステムには任意のアバターを使用した通信システム、モーションキャプチャ機能やボイスチャット機能、デスクトップでログインできる機能が搭載されており、所属サークルのバーチャル部会を開いたそうです。将来的にはVRMMORPGを作成したいとのこと。

前期よりも発展的な内容や、自分のやってみたいことにチャレンジした学生が多く見受けられたように感じます。他の授業の課題やテストに追われつつも、クオリティの高い制作を行ってきた学生たちの作品にとても感心しました。是非、これからも電通生らしいものづくりを続けていってほしいなと感じました。

FPGAテトリス(2020/2/5)

情報数理工学/コンピュータサイエンス実験第二の4ラウンド目には「FPGAテトリス」と呼ばれる課題があります。この課題は名前の通りFPGA(書き換え可能なハードウェア)でテトリスをつくる課題です!

テトリス課題ではVerilogと呼ばれる言語を使って、音を生成するモジュール、画面に映像を映す信号を生成するモジュールを作り、それらが完成してからFPGAボードのボタンで操作できるテトリスを作ります。

課題は全7回の授業から構成されていて、最初の1、2回目で音声モジュールの設計をし、3、4回目では映像出力モジュールの設計、5、6回目でテトリスのゲームを実装して、最終回では学生がそれぞれ自分の作ったテトリスについて発表をします。

テトリス課題では下の写真のFPGAボード(Xilinx社のBasys 3)とサウンドブザーを使用します。

Verilogのコードを書いたら専用のツールを使ってコンパイルします。コンパイルして出来たファイルはPCと接続したFPGAに書き込むことで動かすことができます。

発表は一人10分程度で行い、学生はデモ発表に加えて、自分のFPGAテトリスで工夫した部分や、FPGAテトリスを作る上で頑張ったこと、苦労したことについて発表します。

この課題は音楽モジュール、映像信号モジュール、テトリス回路を6回の授業で実装するので、学生はハードなスケジュールでテトリスを作る必要がありましたが、発表の時点では個性的な作品が多くみられました。

テトリス課題はFPGA初心者でも楽しめる課題です。これから実験第二を履修する方は是非テトリス課題を選んでみてはいかがでしょうか?

情報工学工房ダンボールコミュニケーションロボットチーム後期活動紹介(2019/10/30)

こんにちは。I類(情報系)計算機実験室管理者の島崎です。本日は、情報工学工房ダンボールコミュニケーションチームの活動を報告します。これがダンボールコミュニケーションロボットです(顔は作成中)。

ダンボールコミュニケーションロボットは、Raspberry Pi と呼ばれる小さいコンピュータからできています 。Googleの音声認識機能を用いて、様々なサービスを作ることができます。

ダンボールコミュニケーションロボットチームは、1年生から大学院生まで様々な学生が毎週集まって、ロボット作成に必要な技術を自主的に勉強しています。

実際に、学生が作っているダンボールコミュニケーションロボットは様々。
1年生から3年生まで様々な類の学生や大学院生と一緒に学んでいます!

ダンボールコミュニケーションロボットチームは、電気通信大学図書館のAgoraと呼ばれる学修スペースで毎週水曜の5限に活動しています。

ダンボールコミュニケーションチームは、庄野逸教授、モバイルクリエイト株式会社のエンジニア山口さんのご協力で運営しています。講義と違い皆でディスカッションしながら楽しむことを大切にしています。

それぞれの学生が設計したユニークな制作物は、11月以降に紹介する予定です。

情報工学工房では、電気通信大学の学園祭(調布祭)と同時開催のオープンキャンパス(2019/11/24)も様々なテーマの学生さんが制作物を発表する予定です。https://www.uec.ac.jp/opencampus/

是非、ご覧ください!