diff --git a/src/docs/chapter/other/Jens_Bendisposto_Conferences.adoc b/src/docs/chapter/other/Jens_Bendisposto_Conferences.adoc deleted file mode 100644 index a6b229ae6bd103c0de67f51db12264202c60df28..0000000000000000000000000000000000000000 --- a/src/docs/chapter/other/Jens_Bendisposto_Conferences.adoc +++ /dev/null @@ -1,70 +0,0 @@ - -== Conferences - -* *VMCAI* International Conference on Verification, Model Checking, -and Abstract Interpretation http://vmcai13.di.univr.it/Home.html -* *CAV* International Conference on Computer Aided Verification -http://cav12.cs.illinois.edu/cfp.html -* *TCAS* International Conference on Tools and Algorithms for the -Construction and of Analysis Systems http://www.etaps.org/2012/tacas -http://www.etaps.org/2012/call-for-papers -* *FMCAD* International Conference on Formal Methods in -Computer-Aided Design http://www.cs.utexas.edu/users/hunt/FMCAD/ -* *FTSCS* International Workshop on Formal Techniques for -Safety-Critical Systems -http://www.ftscs.org/2012/index.php?n=Conference.CallForPapers -* *ICST* International Conference on Software Testing, -Verification, and Validation -http://www.icst.lu/site/icst2013/call-for-papers -* *INFINITY* International Workshop on Verification of Infinite-State -Systems http://www.it.uu.se/workshop/infinity2012/ -* *DATE* Design Automation and Test in Europe -http://www.date-conference.com/ -* *MoTiP* Workshop on Model-based Testing in Practice -http://www.ourglocal.com/event/?eventid=19009 -* *ACES-MB* Workshop on Model Based Architecting and Construction -of Embedded Systems -http://www.artist-embedded.org/artist/Overview,2130.html -* *SIGSOFT* International Symposium on the Foundations of Software -Engineering http://sel.ifmo.ru/esec-fse2013/ -* *ISoLA* International Symposium on Leveraging Applications of -Formal Methods, Verification, and Validation -http://www.cs.uni-potsdam.de/isola/isola2012/pdf/isola-cfp2012.pdf -* *ASE* International Conference on Automated Software Engineering -http://ase2012.paluno.uni-due.de/calls/ -* *FASE* International Conference on Fundamental Approaches to -Software Engineering http://www.etaps.org/2012/fase -http://www.etaps.org/2012/call-for-papers -* *PLDI* Conference on Programming Language Design and -Implementation http://pldi12.cs.purdue.edu/content/calls-征稿启事 -* *ICSE* International Conference on Software Engineering -http://2013.icse-conferences.org/submissions -* *SAS* Static Analysis Symposium -http://www.sas2012.ens.fr/#submission -* *FM* International Symposium on Formal Methods -http://www.fmeurope.org/?p=443 -* *SPIN* International SPIN Workshop on Model Checking of Software -http://qav.cs.ox.ac.uk/spin2012/ -* *ATVA* International Symposium on Automated Technology for -Verification and Analysis http://www.iarcs.org.in/atva2012/ -* *AVOCS* International Workshop on Automated Verification of -Critical Systems http://www.swt-bamberg.de/AVoCS2012/callforpapers.php -* *PDMC* International Workshop on Parallel and Distributed Methods -in Verification http://www.pdmc.cz/PDMC12/ -* *BMC* International Workshop on Bounded Model Checking -http://www.illc.uva.nl/LogicList/newsitem.php?id=1835 -* *MoChArt* Model Checking and Artificial Intelligence -http://www.aaai.org/Workshops/ws13.php -* *SBFM* Workshop on Systems Biology and Formal Methods -http://cs.nyu.edu/~pcousot/SBFM2012/index.html -* *MoCSeRS* Workshop on model checking secure and reliable systems -http://www.comp.nus.edu.sg/~pat/MoCSeRS2010/submission.html -* *ICFEM* International Conference on Formal Engineering Methods -http://www.jaist.ac.jp/icfem2012/callforpapers/index.html -* *DSN* International Conference on Dependable Systems and Networks -http://2013.dsn.org/call-for-contributions/ -* *MBT* Model Based Testing, Satellite workshop of ETAPS European -joint conference on Theory And Practice of Software -http://mbt-workshop.org/ -* *SoftMC* Workshop on Software Model Checking -http://www.cav2005.inf.ed.ac.uk/2005_call_for_papers.html diff --git a/src/docs/chapter/other/Jens_Bendisposto_Model_Checkers.adoc b/src/docs/chapter/other/Jens_Bendisposto_Model_Checkers.adoc deleted file mode 100644 index 0b83da6c68f6f119fed09e7f5eeb784f67c89c26..0000000000000000000000000000000000000000 --- a/src/docs/chapter/other/Jens_Bendisposto_Model_Checkers.adoc +++ /dev/null @@ -1,32 +0,0 @@ - -== Model Checkers - -* *SPIN* http://spinroot.com/spin/whatispin.html -* *PAT* http://www.comp.nus.edu.sg/~pat/ -* *MALPAS* -http://www.atkinsglobal.co.uk/sectors-and-services/sectors/defence/documents/~/media/Files/A/Atkins-UK/Attachments/sectors/defence/library-docs/capability-statements/malpas.pdf -* *Mocha* http://www.cis.upenn.edu/~mocha/ -* *Prism* http://www.prismmodelchecker.org/ -* *NuSMV* http://nusmv.fbk.eu/ -* *PVS* http://pvs.csl.sri.com/ -* *COMPASS* http://compass.informatik.rwth-aachen.de/about.html -* *COSPAN* -* *SMV* Symbolic Model Verifier -http://www.cs.cmu.edu/~modelcheck/smv.html -http://www.kenmcmil.com/smv.html -* *NuSMV* http://nusmv.fbk.eu/ -* *Murphi* http://www.cs.utah.edu/formal_verification/Murphi/ -* *XMC* http://www.cav2005.inf.ed.ac.uk/2005_call_for_papers.html -* *BLAST* http://mtc.epfl.ch/software-tools/blast/index-epfl.php -* *DiVinE* http://divine.fi.muni.cz/ -* *Solibri* http://www.solibri.com/ -* *Bogor* http://bandera.projects.cis.ksu.edu/ -http://bogor.projects.cis.ksu.edu/ -* *MCK* http://cgi.cse.unsw.edu.au/~mck/pmck/ -* *YASM* http://www.cs.toronto.edu/~arie/yasm/ -* *SLAM* http://research.microsoft.com/en-us/projects/slam/ - -Other Lists: - -* http://www.pst.informatik.uni-muenchen.de/~hammer/mc-list.html -* http://en.wikipedia.org/wiki/List_of_Model_Checking_Tools diff --git a/src/docs/chapter/reference/01_ABZ14.adoc b/src/docs/chapter/reference/01_ABZ14.adoc deleted file mode 100644 index 451e7dd5f9f2830f0955c0040a85ad88f54345e1..0000000000000000000000000000000000000000 --- a/src/docs/chapter/reference/01_ABZ14.adoc +++ /dev/null @@ -1,72 +0,0 @@ -[[abz14]] -== ABZ 2014 Case Study - -This page provides additional resources for the journal article we have submitted for the -http://sttt.cs.uni-dortmund.de/[International Journal on Software Tools for Technology Transfer]. - -The journal article is an extended version of the paper we have submitted for the -http://www.irit.fr/ABZ2014/casestudy.html[ABZ 2014 case study track]. - -The full description of the case study can be found https://www3.hhu.de/stups/prob/images/d/df/Landing_system.pdf[here] - -[[prob-live-visualisations]] -=== ProB Live Visualisations - -We have prepared two interactive live visualizations of the case study. -One of our own Event-B model and one of the first development by -Jean-Raymond Abrial and Wen Su footnote:[Aircraft Landing Gear System: -Approaches with Event-B to the Modeling of an Industrial System, Su, W. -and Abrial, J., 2014 in Communications in Computer and Information -Science (ABZ 2014: The Landing Gear Case Study)]. - -The visualization of our own model can either be controlled by -interacting with the displayed elements (i.e., clicking the handle) or -using the Events view which can be opened using the "Open View" menu -at the bottom right corner. The other model can only be controlled using -the Events view. - -http://wyvern.cs.uni-duesseldorf.de/bms/landing.html[Visualization of our own model] - -1. http://wyvern.cs.uni-duesseldorf.de:18080/bms/vis_dev1_fixed/landinggear.html[Visualization -of the model by Jean-Raymond Abrial and Wen Su (Temporally disabled)] - -[[bmotion-studio-for-prob-video]] -=== BMotion Studio for ProB Video - -ifdef::basebackend-html[] -++++ -<script> -video::wFr_pEjbpqo[youtube] -</script> -++++ -endif::[] - -You can find the video https://youtu.be/wFr_pEjbpqo[here]. - - -=== Resources - - -* https://www3.hhu.de/stups/downloads/pdf/abz14casestudy.pdf[ABZ 2014 Case Study Paper] - -* https://www3.hhu.de/stups/prob/images/7/77/LandingGear.zip[Landing Gear Model EventB Model] - -=== Links - -[[bmotion-studio-for-prob]] -==== BMotion Studio for ProB - - -* https://www3.hhu.de/stups/prob/index.php/BMotion_Studio[BMotion Studio -for ProB Homepage] -* https://www3.hhu.de/stups/handbook/bmotion/current/html[BMotion Studio -for ProB User Handbook] -* https://github.com/ladenberger/bmotion-prob[BMotion Studio for ProB -Sourcecode] - -[[prob-2.0]] -==== ProB 2.0 - -* https://github.com/bendisposto/prob2[ProB 2.0 Sourcecode] -* https://www3.hhu.de/stups/downloads/[ProB 2.0 Downloadsite] -* https://www3.hhu.de/stups/handbook/prob2/prob_tcltk.html[ProB 2.0 User Manual] diff --git a/src/docs/chapter/reference/02_ABZ16.adoc b/src/docs/chapter/reference/02_ABZ16.adoc deleted file mode 100644 index ad5c43bd4e7c6fc7d8e8f97de6dbfafd294e2ac1..0000000000000000000000000000000000000000 --- a/src/docs/chapter/reference/02_ABZ16.adoc +++ /dev/null @@ -1,51 +0,0 @@ -[[abz16]] -== ABZ 2016 Case Study - -[[the-hemodialysis-machine-case-study]] -=== The Hemodialysis Machine Case Study - -This page provides additional information and resources for the paper we -have submitted for the http://www.cdcc.faw.jku.at/ABZ2016[ABZ 2016 case study track]. - -The full description of the case study can be found http://www.cdcc.faw.jku.at/ABZ2016/HD-CaseStudy.pdf[here]. - -==== Resources - -* http://www.cdcc.faw.jku.at/ABZ2016/HD-CaseStudy.pdf[ABZ 2016 Case Study Paper] - -The original specification of the HD machine as PDF. - -* https://www3.hhu.de/stups/prob/images/d/d3/HDMachine-160122.zip[HD Machine Event-B Model] - -The zip file contains the HD machine Event-B model. You can import the -zip file directly into the Rodin platform as an Event-B project. - -* https://www3.hhu.de/stups/prob/images/b/bf/Cosim-160122.zip[Co-Simulation Model of the Blood Flow Control] - -The zip file of the co-simulation model contains a readme file that -explains what is included. - -* https://www3.hhu.de/stups/prob/images/3/39/HDMachine-BMS-160122.zip[BMotion Studio Visualisation] - -The zip file contains the domain specific visualisation of the HD -machine developed with BMotion Studio. You need to -https://www3.hhu.de/stups/prob/index.php/BMotion_Studio[download] -the latest version of BMotion Studio (v.0.2.7). Some instruction for -getting started with BMotion Studio can be find -http://www3.hhu.de/stups/handbook/bmotion/current/html/first_steps.html[here]. - -[[live-visualisation]] -==== Live Visualisation - -* http://wyvern.cs.uni-duesseldorf.de/bms/hdmachine.html[BMotion Studio -Visualisation of the HD Machine] - -If you have problems in running the visualisation, please contact Lukas -Ladenberger (ladenberger@cs.uni-duesseldorf.de) - -==== Links - -* https://www3.hhu.de/stups/prob/index.php/BMotion_Studio[BMotion Studio for ProB Homepage] -* https://www3.hhu.de/stups/handbook/bmotion/current/html[BMotion Studio for ProB User Handbook] -* http://wiki.event-b.org/index.php/IUML-B[iUML-B Homepage] -* https://www3.hhu.de/stups/handbook/rodin/[Rodin Handbook] diff --git a/src/docs/chapter/reference/03_FormalPrototyping.adoc b/src/docs/chapter/reference/03_FormalPrototyping.adoc deleted file mode 100644 index 876884ecc79fbc13a3923d54fa093d6b74d6408f..0000000000000000000000000000000000000000 --- a/src/docs/chapter/reference/03_FormalPrototyping.adoc +++ /dev/null @@ -1,53 +0,0 @@ -[[formal_prototyping]] -== Formal Prototyping - -This page provides additional information and resources for the tool paper -we have submitted for the http://staf2016.conf.tuwien.ac.at/sefm/[SEFM 2016 conference]. - -=== Resources - -* https://www3.hhu.de/stups/prob/index.php/BMotionWeb_Download[BMotionWeb Download] -* https://www3.hhu.de/stups/prob/images/d/de/Phonebook.Formal.Prototype.zip[Phonebook Formal Prototype] -* https://www3.hhu.de/stups/prob/images/1/1a/CCS.Formal.Prototype.zip[Cruise Control System Formal Prototype] - -[[live-online-formal-prototypes]] -=== Live Online Formal Prototypes - -* http://wyvern.cs.uni-duesseldorf.de/bms/phonebook.html[Phonebook Online-Version] -* http://wyvern.cs.uni-duesseldorf.de/bms/ccs.html[Cruise Control System Online-Version] - -Please note, that the visual editor is only available in the -desktop-version of BMotionWeb. - -If you have troubles with running the online version, please contact -Lukas Ladenberger (ladenberger@cs.uni-duesseldorf.de). - -=== Links - -* https://www3.hhu.de/stups/prob/index.php/BMotion_Studio[BMotionWeb Homepage] -* https://www3.hhu.de/stups/handbook/bmotion/current/html[BMotionWeb User Handbook] - -[[getting-started-with-bmotionweb]] -=== Getting Started with BMotionWeb - -WARNING: BMotionWeb is currently not up-to-date and not in use anymore. BMotion Studio however can still be downloaded with our ProB Plugin for Rodin. - -[[install-bmotionweb]] -==== Install BMotionWeb - -Start off by downloading BMotionWeb for your operating system. -Decompress the archive and expand the directory if necessary. Navigate -to the application folder and start BMotionWeb by executing the -bmotion-prob binary. - -[[open-a-formal-prototype]] -==== Open a Formal Prototype - -Start off by downloading a formal prototype from this wiki page. -Decompress the archive and expand the directory if necessary. To open a -formal prototype, click on the box in the middle of the window and -select the BMotionWeb manifest file (.json file) of the formal prototype -or just drag and drop the manifest file into the box. You can also open -a formal prototype via the top menu: File > Open Visualization. For -instance, to load the phonebook or CCS formal prototype select the -phonebook.json or ccs.json file respectively. diff --git a/src/docs/chapter/reference/04_ProjectionDiagram.adoc b/src/docs/chapter/reference/04_ProjectionDiagram.adoc deleted file mode 100644 index feb24f89157a8c4b59196181df331c25d779e552..0000000000000000000000000000000000000000 --- a/src/docs/chapter/reference/04_ProjectionDiagram.adoc +++ /dev/null @@ -1,43 +0,0 @@ -[[projection-diagram]] -== Mastering the Visualization of Larger State Spaces with Projection Diagrams - -NOTE: This page provides additional resources for the paper for http://icfem2015.lri.fr/[ICFEM 2015]. - -[[resources-and-prob-live-visualizations]] -=== Resources and ProB Live Visualizations - -We have prepared two interactive live visualizations. One of the Event-B -model of the landing gear system (the full description of the case study -can be found https://www3.hhu.de/stups/prob/images/d/df/Landing_system.pdf[here]) and one of the Event-B -model of a simple lift system. - -The visualizations can either be controlled by interacting with the -displayed elements (i.e., clicking the handle) or using the Events view -which can be opened using the "Open View" menu at the bottom right -corner. - -1. http://wyvern.cs.uni-duesseldorf.de/bms/landing.html[Visualization -of the landing gear system] -2. http://wyvern.cs.uni-duesseldorf.de/bms/lift.html[Visualization of -the simple lift] - -The Event-B model of the simple lift system be can be downloaded https://www3.hhu.de/stups/prob/index.php/File:SimpleLift.zip[here]. - -http://stups.hhu.de/w/Special:Publication/LadenbergerLeuschel_ProjectDiagram[Technical -Report] - -[[creating-a-domain-specific-projection]] -==== Creating a Domain Specific Projection - -* Open the ModelCheckingUI using the "Open View" menu at the bottom -right corner. -* Click on the "MC" icon and run the model checker in order to explore -the full state space of the model. -* After finishing, you can open the Element Projection view using the -"Open Diagram" menu at the bottom right corner. -* Select the lift or landing visualization respectively and select some -elements for the projection. - -Please note: Due to a small bug, you can only create a projection for -max. two selected graphical elements at the moment. We are already -working on this bug. diff --git a/src/docs/chapter/reference/05_Sefm2015.adoc b/src/docs/chapter/reference/05_Sefm2015.adoc deleted file mode 100644 index 1134972b14a5bd69b1cc91f853816efbc339c4ba..0000000000000000000000000000000000000000 --- a/src/docs/chapter/reference/05_Sefm2015.adoc +++ /dev/null @@ -1,77 +0,0 @@ -[[sefm2015]] -== Benchmarks for the ProB (Dis)prover - -We benchmarked the ProB disprover for an article for SEFM 2015. - -=== Raw Data - -All raw data is available as csv files from -https://www3.hhu.de/stups/models/sefm2015_disprover/raw/[here]. -A zip file containing all csv files is available -https://www3.hhu.de/stups/models/sefm2015_disprover/raw/rawdata.zip[here]. - -=== Data Visualisations - -Due to the page limit, we could not give all the diagrams and -visualisation of the benchmark results in the article. They are -available here: - -==== Landing Gears - -* https://www3.hhu.de/stups/models/sefm2015_disprover/output/abrial1_provers_only.pdf[Su -and Abrial, Landing Gear Model 1, Provers alone] -* https://www3.hhu.de/stups/models/sefm2015_disprover/output/abrial1_tactic.pdf[Su -and Abrial, Landing Gear Model 1, Tactics] -* https://www3.hhu.de/stups/models/sefm2015_disprover/output/abrial2_provers_only.pdf[Su -and Abrial, Landing Gear Model 2, Provers alone] -* https://www3.hhu.de/stups/models/sefm2015_disprover/output/abrial2_tactic.pdf[Su -and Abrial, Landing Gear Model 2, Tactics] -* https://www3.hhu.de/stups/models/sefm2015_disprover/output/abrial3_provers_only.pdf[Su -and Abrial, Landing Gear Model 3, Provers alone] -* https://www3.hhu.de/stups/models/sefm2015_disprover/output/abrial3_tactic.pdf[Su -and Abrial, Landing Gear Model 3, Tactics] -* https://www3.hhu.de/stups/models/sefm2015_disprover/output/landinggearfinal_provers_only.pdf[Hansen -et. al., Provers alone] -* https://www3.hhu.de/stups/models/sefm2015_disprover/output/landinggearfinal_tactic.pdf[Hansen -et. al., Tactics] -* https://www3.hhu.de/stups/models/sefm2015_disprover/output/mammarlaleau_provers_only.pdf[Mammar -and Laleau, Provers alone] -* https://www3.hhu.de/stups/models/sefm2015_disprover/output/mammarlaleau_tactic.pdf[Mammar -and Laleau, Tactics] -* https://www3.hhu.de/stups/models/sefm2015_disprover/output/nantes_provers_only.pdf[André, -Attiogbé and Lanoix, Provers alone] -* https://www3.hhu.de/stups/models/sefm2015_disprover/output/nantes_tactic.pdf[André, -Attiogbé and Lanoix, Tactics] - -==== Further Models - -* https://www3.hhu.de/stups/models/sefm2015_disprover/output/canbus_provers_only.pdf[Colley, -Canbus, Provers alone] -* https://www3.hhu.de/stups/models/sefm2015_disprover/output/canbus_tactic.pdf[Colley, -Canbus, Tactics] -* https://www3.hhu.de/stups/models/sefm2015_disprover/output/graphcoloring_provers_only.pdf[Andriamiarina -and Méry, Graphcoloring, Provers alone] -* https://www3.hhu.de/stups/models/sefm2015_disprover/output/graphcoloring_tactic.pdf[Andriamiarina -and Méry, Graphcoloring, Tactics] -* https://www3.hhu.de/stups/models/sefm2015_disprover/output/graphcoloring_provers_only.pdf[Wiegard, -Stuttgart 21, Provers alone] -* https://www3.hhu.de/stups/models/sefm2015_disprover/output/graphcoloring_tactic.pdf[Wiegard, -Stuttgart 21, Tactics] - -==== Summaries - -* https://www3.hhu.de/stups/models/sefm2015_disprover/output/tactic_landiggears.pdf[Tactics -on Landing Gears] -* https://www3.hhu.de/stups/models/sefm2015_disprover/output/tactic_all_models.pdf[Tactics -on all Models] -* https://www3.hhu.de/stups/models/sefm2015_disprover/output/provers_alone_landiggears.pdf[Provers -alone on Landing Gears] -* https://www3.hhu.de/stups/models/sefm2015_disprover/output/provers_alone_all_models.pdf[Provers -alone on all Models] - -==== Surplus of ProB - -* https://www3.hhu.de/stups/models/sefm2015_disprover/output/surplus.pdf[Surplus -of ProB (added last)] -* https://www3.hhu.de/stups/models/sefm2015_disprover/output/surplus2.pdf[Surplus -of ProB (added first)]