タグ

2020年2月27日のブックマーク (2件)

  • SWETグループが考える形式手法の現在とこれからの可能性 - DeNA Testing Blog

    こんにちは、SWETの鈴木穂高(@hoddy3190)です。 私は、こちらの記事で紹介されているようなAndroidテストの教育活動をする傍ら、形式手法という技術の可能性を模索しています。 今回は、形式手法についての簡単な説明や、調べていくにつれてわかってきた実用可能性等をご紹介できればと思います。 動機 まず、なぜ私が形式手法について調べようと思ったのかをご説明します。 SWETに所属する前、私は、別の部署で4年ほどゲーム開発に携わっていました。 そこでよく課題に感じていたのは、日語で書かれる仕様の不備(考慮漏れ、記載漏れ、矛盾など)により、大きな手戻りにつながることが多いということでした。 開発プロセス上でそのような問題が発生すると、当然再発防止策MTGが開かれます。 有識者のレビューを開発フェーズのより早い段階で組み込むようにするフロー改善や、 考慮漏れを防ぐためのチェックリストな

    SWETグループが考える形式手法の現在とこれからの可能性 - DeNA Testing Blog
  • 形式手法のこれまでとこれから - ヾノ*>ㅅ<)ノシ帳

    2019年が終わろうとしています あけおめ~さて2020年になりました。歴史が長い形式手法の今後を占うため、過去と直近の出来事を振り返りたいと思います。 ツッコミやタレコミは私のTwitter宛かあなたのブログかその他経路でお願いします~ シンボリック実行は形式的であるため稿では形式手法に含めることにします。 Fuzzing関連はサーベイが甘いので漏れが多いかもしれません。 形式手法・形式検証とは 形式検証とは、厳密に定義された意味論の下で仕様やプログラムが所定の性質を満たすことを形式的に検証するための手法をいいます。「形式的に」とは、検証が事前に定義された知識だけに基づいており、検証手順が決定的であることをいうと私は理解しています。 形式手法は、形式検証に加えて、形式的にプログラムの仕様を厳密に定義するための手法を包含します。 記事では形式手法を以下の通り大きく3つに独自に分類します

    形式手法のこれまでとこれから - ヾノ*>ㅅ<)ノシ帳