モデル検査

プログラミングは
書いては間違いを
見つけて直す、
の繰り返し。

最初は楽しくやっているけれど、だんだん辛くなってきませんか。そんな状況を少しでも楽にしたい。間違いを直すお手伝いをいたします。直し方を教えることはできないけれど、せめて間違いを見つけることはやりましょう。仕様を教えてもらえれば、隠れた小さなバグも見つけます。

#モデル検査#形式手法 #formalmethods #modelchecking #欠陥の発見 #defectsdiscovery#cornercases#コーナーケース#temporallogic#時相論理

フォーマル

フォーマルスペックは、
きっちり、
でもちょっと
難しくて味気ない。
そんなイメージを
持っていませんか？

書ける
わかる
使える

フォーマルスペックがシステム開発をわかりやすくします。モノを作る流儀は大きく2つに分けられます。きっちりと設計図を書いてから、図面通りのモノを正確に作るやり方。もう1つは、作りながら、少しずつ使ってみながら、完成させるやり方。フォーマルスペックは、両者を両立させたシステム開発を可能にします。

#フォーマルメソッド#formalmethods#形式手法の民主化 #formalmethodsforall #形式仕様 #formalspecifications #ライブ #liveness #探索的仕様記述 #exploratoryspecification #妥当性 #validity #正当性検証 #verification

クリエイティビティの支援

創造的であることは難しい。

思いついたことを試して、失敗して、たまに少し成功して、また試す。時には過去に思いついたことを見直したり、昔諦めたことをもう一度考え直したり。そんな時には、履歴を記録して掘り起こしましょう。履歴を残し忘れた時でも大丈夫。自動的に記録して残します。取り出した履歴の活用までも手助けします。別の履歴とくっつけたり、削除したり、試行錯誤を再現できます。創造的な仕事が楽に、そして楽しくなってきますよ。

#クリエイティビティ#プロトタイピング#prototyping#試行錯誤#開発履歴 #創造性 #creativity #履歴 #history #探索 #exploration #再現性 #reproducibility #検証 #verificationandvalidation

モビリティ

動きって見えないものと
思っていませんか？

人の動き、乗り物の動き、目に映っているようで、一瞬で消え去っていく。そんな不思議なものですが、動いた跡は残ります。行動履歴、移動履歴、年表。それらを見せる技術があります。でも、ただ見せるだけでは面白くない。もっと生き生きと、まるで追体験するように。あなたの足跡だけでなく、他の人との関係も見えるように。常に新しい見せ方を探っています。

#モビリティ#MaaS#移動履歴#探索#可視化#mobility #位置情報 #location #地理情報 #geography #時系列情報 #timeseries #時空間 #timespace #移動 #transportation

可視化

日常にはデータが
溢れています。

バスでの移動、散歩コース、買い物にめぐったお店など、デジタル化される日々の行動を集めて可視化すると、自分の記録がたどれます。日常生活だけでなく様々な環境において行動の記録が作られていきます。ソフトウェア開発環境においてもいろいろな行動履歴が作られます。形式手法の可視化から、検査の自動化までソフトウェア開発に取り組む中で、すばやくフィードバックするライブ感を大切に、ビッグデータ可視化、専門的なシミュレーション、iOSのタッチインタラクティビティ、VRやARなど幅広く探索しています。

#可視化#履歴の可視化#インタラクション#ビッグデータ #visualisation #行動 #behaviours #インタラクティビティ #interactivity#lifelog#ライフログ

お問い合わせはこちら

モデル検査

フォーマル

書けるわかる使える

クリエイティビティの支援

モビリティ

可視化

書ける
わかる
使える