How to escape characters in Haskell's Text.Regex library? - Stack Overflow > matchRegex (mkRegex "[*]") "*" Just [] which works, but it seems like a hack, especially if I want to escape several things in a row (e.g. mkRegex "[[(][)]]" whic…
Common Bugs in WritingEditorial Rules
git で add をすると以下のWarning がでた。 git warning: LF will be replaced by CRLF in 以下の情報が解決に役立った。Git for Windows でレポジトリー上の CR LF を LF に変換する手順 - てっく煮ブログ
~/.bash_profile に以下を記載すると反映されるようになった。 if [ -e ~/.bashrc ] ; then source ~/.bashrc fi より詳しくは、以下を参考にした。 cygwin bashrc エイリアスがうまくできない 【OKWAVE】 Cygwin Bash Shellアイコンをダブルクリックすると…
サルでもわかるGit入門〜バージョン管理を使いこなそう〜【プロジェクト管理ツールBacklog】
http://githowto.com/undoing_staged_changes
http://tech-tec.com/archives/107http://tech-tec.com/archives/107 結論を先に今回は込み入った説明にもなるので先に結論を言ってしまいます。 Windowsではgit config –global core.autocrlf true MacやLinuxではgit config –global core.autocrlf inputと…
lists all the files being tracked by your git repo. git ls-tree --full-tree -r HEAD
gitのリモートリポジトリの更新を確認する - Qiita方法1の後、pull するとローカルに反映される。 gitのリモートリポジトリが更新されているかどうかを確認する方法はいくつかあります。方法1: git fetch 後にdiffをとる $ git fetch origin $ git diff orig…
Open Source Initiative for Automotive Software Development Tools http://wiki.eclipse.org/Auto_IWG#Objectives ObjectivesInnovation in the automotive industry is mostly achieved by electronics and software functions. The system automobile is…
CBMC(C Bounded Model Checker) を試した。windows+cygwin では、うまくできなかった。Parsing のエラーが出た。Ubuntu ではすぐにできた。以下にインストールメモを残す。まずは、インストール。 > apt-get install cbmc 例として、以下のファイル file1.c …
Automated Test Generation using CBMC (Bounded Model Checking for C programs) to reach full Modified Condition/Decision Coverage.
http://www.claudiodesio.com/ooa&d/UMLSR_EN/DSR/ACTD.htm @startuml start :ClickServlet.handleRequest(); :new page; if (Page.onSecurityCheck) then (true) :Page.onInit(); if (isForward?) then (no) :Process controls; if (continue processing?) …
Another possibility is to align misuse cases with traditional fault-tree analysis methods from the safety area, such as threat trees [49] or attack trees [50, 51]. Adapted for security analysis, these trees would decompose security threats…
Fault trees are classified according to their logic function. If during fault tree construction only AND gates and OR gates are used, the resulting fault tree is defined as coherent. If NOT logic is used or directly implied, the resulting …
Minimal Cut Sets Traditional solution of reliability block diagrams and fault trees involves the determination of the so-called minimal cut sets. Cut sets are the unique combinations of component failures that can cause system failure. Spe…
同時にに変数の値を変える nusmv コード MODULE main VAR var1 : boolean; var2 : boolean; ASSIGN init(var1) := TRUE; next(var1) := case TRUE : {TRUE, FALSE}; esac; init(var2) := TRUE; next(var2) := case TRUE : {TRUE, FALSE}; esac;実行例 NuSMV …
■モデル検査と形式証明 モデル検査と形式証明は形式検証技術の主要な技術である。一般に、型式証明は「安全性証明」と言われているが、具体的に「安全性証明」というものは存在せず、「デッドロックがない」とか「ブレーキを踏むと必ずブレーキランプが点灯…
ペアワイズ法は多くのバグを検出できるが、バグがないことを示すものではない。一般的な方法でバグ検出率が高い方法。こうした技術はシステムが一定の品質基準（網羅基準、または社内の品質基準）を満たすことを示すために用いるのに都合が良い。品質基準を…
VirtualBox において、ゲストOSの解像度の調整をしたい。以下の方法を試すが、「VirtualBoxのメニューから「Devices」→「Install Guest Addsinions」をクリックします。」の時点で、「マウントできません（could not mount media）」とエラーが出てしまう。 …
The following code shows a sample of calling a program in Haskell code. It works with compilation (i.e., >ghc CallSATSolver.hs) but not GHCI. import System.Exit import System.Process import Control.Monadmain :: IO () main = do putStrLn "Ru…
The result of planner in the visual viewSamaneh Soltani, Mohsen Asadi, Dragan Gasevic, Marek Hatala, Ebrahim Bagheri: Automated planning for feature model configuration based on functional and non-functional requirements. SPLC (1) 2012: 56…
Haskell parsec で命題論理（propositional logic）の構文解析器を作ってみた。作ってみた、とは一言っても、つくりかけ。BNF の右辺が２つの時はできるのだけど、それが３つ以上になった時にどうして良いかわからない。以下を参考に作った。以下と違って、…
The main challenge of this study was to model the input space in terms of a set of parameters and values. Once the model was designed,we generated test cases using ACTS, which were then later used to test ACTS
An Integrated Approach for Combining BDDs and SAT Provers, by Rolf Drechsler, Gorschwin Fey, and Sebastian Kinder FACTA UNIVERSITATIS (NIS)ˇSER.: ELEC. ENERG. vol. 20. no. 3, December 2007, 415-436 The two most frequently used methods are …
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.
