タグ

formal methodに関するvanbraamのブックマーク (5)

  • 《日経Robo》ファナックが買収したロボベンチャー、ソフトの技術力で群を抜く

    ファナックが2018年2月に買収したロボットベンチャーのライフロボティクス。伸縮式の機構を採用することでロボットの肘関節をなくし、省スペースに設置できる協働ロボット「CORO」を手掛ける(図1)。 トヨタ自動車や外大手の吉野家、ロイヤルホストなどが相次いで自社工場・店舗への採用を決定するなど、注目が高まりつつある(導入事例の記事)。 このライフロボティクスというベンチャー、実はロボットのハードウエア面だけでなく、ロボットに組み込むソフトウエアの面でも、その開発において先駆的なアプローチを取り入れている。それが「形式手法(formal methods)」である。 形式手法は日ではあまり知られていないが、システムやソフトウエアの仕様を厳密に記述し、仕様の品質を高めるための手法である(形式手法については、筆者が2005年に執筆した特集記事「ソフトウエアは硬い」を参照)1)。プログラムなど実装

    《日経Robo》ファナックが買収したロボベンチャー、ソフトの技術力で群を抜く
    vanbraam
    vanbraam 2018/03/30
    国内では稀な形式手法の話;今後ロボットと人との関わりが深くなるにつれて,安全性の面から設計の厳密さは重要になって来そう;曖昧さを統計的に扱うAIとはほぼ真逆のアプローチだと思う
  • P言語の素晴らしさについて - kuenishi's blog

    先週Microsoft社がP言語に関するブログ記事を公開し一部界隈で話題となった。 P言語くん pic.twitter.com/uULzxIO4ct— Kuntaro Ishiyama (@_iamkuntao) 2017年3月26日 「いまさら一文字言語かよ…」「何個目だ?」といった批判的諦念的なものから、「RustGoとErlangの間の子みたいなのだなあ」「なんか読みにくい」といった反応が多くこの言語の重要性やインパクトに対して正しく理解しているものがあまりなかった。尊敬しているTD勢ですらあまり重要性が伝わってないようだ 1 2 。上記のブログ記事を読んだり、マニュアルを読んだらすぐ分かるようなことではあるが、日語で解説しておこうと思う。なおいわゆる言語入門とかそういった類のものではないことをご理解いただきたい。 TL;DR 並行処理や分散システムの形式証明や形式検証はそれ自体

    P言語の素晴らしさについて - kuenishi's blog
    vanbraam
    vanbraam 2017/05/26
    自分が少し知っている(定理証明系の)形式手法と違うと思っていたので,コメントを読んで"パターン網羅系"の形式手法があり,P言語はそちらに属すると知って腑に落ちた
  • 形式手法と AWS のおいしい関係。- モデル検査器 Alloy によるインフラ設計技法 #jawsfesta

    JAWS Festa 東海道 2016 の発表スライドです。モデル検査器 Alloy を用いて AWS のリソースをモデル化し、仕様からインフラ設計を自動で生成する流れをお見せします。Read less

    形式手法と AWS のおいしい関係。- モデル検査器 Alloy によるインフラ設計技法 #jawsfesta
    vanbraam
    vanbraam 2016/10/23
    可視化機能が良さげ;AWS上の様々なサービスのAlloyモデルが,公式から提供されているといいのに
  • 「関数型プログラミングはオブジェクト指向の正当な後継」なの? - 檜山正幸のキマイラ飼育記 (はてなBlog)

    オブジェクト指向を知っている人々に、「関数型もオブジェクト指向と大差ないよ、大丈夫だよ」とお誘いする記事は大いに存在意義があると思います。 関数型プログラミングはオブジェクト指向の正当な後継である 上記の記事は、そういう目的を持って書かれたのでしょう。その内容(目次)は次のようです(僕のこの記事の目次じゃないよ)。 対象読者 なぜこの記事を書こうと思ったのか? なぜ関数型プログラミングはわかりにくいのか? オブジェクト指向の負の遺産を捨てよう 関数型プログラミングの概要 「阿吽の呼吸」とも言うべき使いやすさの拡張 型にまつわる考察 まとめ 最初のほうを読むと、言ってることはまっとうで好感を持てます。が、「5. 関数型プログラミングの概要」の節あたりから雲行きが怪しくなって、ちょっと何言ってるかわかんない((c)サンドウィッチマン)。 檜山のこの記事の内容: 真面目なポエム モナドっておいし

    「関数型プログラミングはオブジェクト指向の正当な後継」なの? - 檜山正幸のキマイラ飼育記 (はてなBlog)
    vanbraam
    vanbraam 2016/09/14
    なるほど.自分が感じていた違和感が言語化されてる.確かに"後継"ではないものを無理に"後継"と呼ぶから変になるのであって,単に似てるとか考え方が応用できるとか書けばあそこまで変な記事にはならないと思った
  • 形式手法で捗る!インフラ構成の設計と検証

    AWS Summit Tokyo 2016 内で行で行われた、JAWS-UG のナイトセミナーで使用したスライドです。形式手法とは何かを簡単に説明した後、具体例としてモデル検査器 Alloy を用いて AWSセキュリティグループを検証します。なお、スライド中に登場するコード断片に対して、完全に検証可能な形に仕上げたものは https://gist.github.com/y-taka-23/89a98fdb2ba48710a39c を参照のこと。

    形式手法で捗る!インフラ構成の設計と検証
    vanbraam
    vanbraam 2016/06/06
    久々の形式手法記事
  • 1