NIST開発のACTSを試す。コマンドラインからの実行は、Cygwin等で以下を実行。 java -Doutput=csv -jar ../acts_cmd_beta_v2_r2.6.jar ActsConsoleManager inputfile.txt ouputfile.csv outputファイルの指定がない場合は、Current にOutput.csv として出力さ…

Marcílio Mendonça, Andrzej Wasowski, Krzysztof Czarnecki: SAT-based analysis of feature models is easy. SPLC 2009: 231-240

Investigating the Influence of Formal Methods Formal methods promise much, but can they deliver? In this project, results are inconclusive, but careful data gathering and analysis helped establish influences on product quality.

I like the following explanation.1 Explain the difference between safety and security Safety is rather protection against accidental events; security is rather protection against intentional damages.Examples:1) In the case of a hurricane a…

C プログラムから Control Flow Graph（CFG）を取り出す必要があり、色々と調べてみた。結果、以下の2つの方法が有望そう。1つはgcc の"-fdump-tree-fixupcfg" オプションを使う方法。もう一つは、Berkley が作っている C Intermediate Language (CIL) を使…

仕様記述言語とプログラミング言語の違いってほとんどないような感じを前々から持っていて、そもそも区別する必要がないんじゃない？と考えていた。そんな折、2011年11月の IEEE Software archive（Volume 28 Issue 6）に「From Programming o Modeling and …

[Frama-c-discuss] frama graph plugins [Frama-c-discuss] frama graph plugins Julien Signoles Julien.Signoles at cea.fr Fri May 28 10:18:43 CEST 2010 Previous message: [Frama-c-discuss] frama graph plugins Next message: [Frama-c-discuss] Non…

gcc -fdump-tree-cfg sample.c

Coflo GCC Python plugin — gcc-python-plugin 0.16 documentation

Microsoft Academic Microsoft Academic- Microsoft Academic Microsoft Academic Microsoft Academic Microsoft Academic Microsoft Academic Microsoft Academic Microsoft Academic Microsoft Academic Microsoft Academic Microsoft Academic Microsoft …

Famous Bisimulation checker Piet Mobility Workbench ABC

On the Adoption of Model Checking in Safety-Related Software Industry Alessandro Fantechi, Stefania GnesiComputer Safety, Reliability, and Security Lecture Notes in Computer Science Volume 6894, 2011, pp 383-396 3.3 Tool Qualification When …

Requirements engineers live in a world where conflicts are the rule, not the exception [Eas94].

A Survey of Combinatorial TestingCHANGHAI NIE, State Key Laboratory for Novel Software Technology, Nanjing University HARETON LEUNG, Hong Kong Polytechnic UniversityACM Computing Surveys, Vol. 43, No. 2, Article 11, Publication date: Janua…

Yin, R. K. (2002) Case Study Research: Design and Methods (3rd Edition). CA:Sage. Stake, R.E. (1995). The art of case study research. Thousand Oaks, CA:Sage. Ragin, C.C., & Becker, H.S. (Eds.). (1992). Whatis a case? Exploring the foundati…

J. W. Duran and S. C. Ntafos. An Evaluation of Random Testing. IEEE Transactions on Software Engineering, pages 438-444, July 1984.ABSTRACTRandom testing of programs has usually (but not always) been viewed as a worst case of program testi…

There exists x such that P(x,y) for any y in Y. For all x in X, there exists y such that P(x,y). There exists x in X such that P(x,y) for some y in Y. For all x in X, P(x,y) for all y in Y.

復刊 数理論理学作者: 松本和夫出版社/メーカー: 共立出版発売日: 2001/08/15メディア: 単行本購入: 3人 クリック: 12回この商品を含むブログ (6件) を見る数理論理学の基本がコンパクトにまとまっている。数理論理学の入門書はたくさんあり、それぞれまとめ…

基本から学ぶソフトウェアテスト作者: Cem Kaner,Hung Quoc Nguyen,Jack Falk,テスト技術者交流会出版社/メーカー: 日経BP社発売日: 2001/11/25メディア: 単行本購入: 5人 クリック: 151回この商品を含むブログ (24件) を見る

■「品質」の分類 これまでに何度か使った「品質」という言葉は非常にあいまいです。実体のあるものとは異なり、目に見えないシステムの品質をイメージするのは困難ですが、システム（正確にいうとソフトウェア）が満たすべき品質は以下の6つに分類されます。…

"Why a Diagram is (Sometimes) Worth Ten Thousand Words" JILL H. LARKIN and HERBERT A. SIMON COGNITIVE SCIENCE 11, 65-99 (1987) We distinguish diagrammatic from sentential paper-and-pencil representations of information by developing altern…

"What Makes a Good Diagram? Improving the Cognitive Effectiveness of Diagrams in IS Development" By Daniel Moodyhttp://www.springerlink.com/content/w3465l78v1728027/ Abstract Diagrams play a critical role in IS development. Despite this, I…

The seven key principles of correct by construction: Expect requirements to change. Know why you're testing. Eliminate errors before testing. Write software that is easy to verify. Develop incrementally. Some aspects of software developmen…

PCを新調（Windows7 64bit SSD）したのですが、NuSMVのBMCが途中で止まってしまう。

Windows 中国語IMEをインストールすると、デフォルトで「ctrl-space」が中国語IMEへの切り替えに割り当てられる。一方で、emacs では「ctrl-space」が set mark に割り当てられているが、、この中国語IMEによって使えなくなってしまう。emacs の set mark を…

pict pict_sample.txt /o3

Boolean Algebra and Logic Gates F Hamer, M Lavelle & D McMullanhttp://www.tech.plym.ac.uk/maths/resources/pdflatex/boolean_alg2.pdf

The problem of generating a minimum test set for pair-wise testing is NP-complete.References: An Improved Test Generation Algorithm for Pair-Wise Testing, by Soumen Maity, Amiya Nayak, Marzia Zaman, Nita Bansal, and Alka Srivastava Lei, Y …

This is a memo of complexity analysis of "checking the existence of counter-example at bound k using bounded model checking with SAT". (And this is different from the complexity of bounded model checking using SAT). In BMC using SAT, model…