From c17f573ea330c307e712e35a53cc26fa2104a873 Mon Sep 17 00:00:00 2001
From: Michael Jastram <michael@jastram.de>
Date: Tue, 24 Sep 2013 10:09:32 +0000
Subject: [PATCH] ProR Chapter

git-svn-id: svn://svn.code.sf.net/p/rodin-b-sharp/svn/trunk/Handbook@15927 1434b563-b632-4741-aa49-43a3a8374d2e
---
 org.rodinp.handbook.feature/latex/img/pror.png | Bin 0 -> 1480 bytes
 .../latex/tutorial-03.tex                      |  17 +++++++++++++++++
 2 files changed, 17 insertions(+)
 create mode 100644 org.rodinp.handbook.feature/latex/img/pror.png

diff --git a/org.rodinp.handbook.feature/latex/img/pror.png b/org.rodinp.handbook.feature/latex/img/pror.png
new file mode 100644
index 0000000000000000000000000000000000000000..b229f9f8e2520d80714e89c2f5ac762f02042b7f
GIT binary patch
literal 1480
zcmeAS@N?(olHy`uVBq!ia0y~yV6XvU4mJh`2CF|eix?Of*pj^6T^Rm@;DWu&Co?cG
za29w(7Bes$DhFZ4(5V~=3=9nHC7!;n>~}dOI5kD@H2=8Iz`z>n>EalYaqsP{>>QC$
ziMIJOBcm2LcSm!%=B@2mD4u2Fnzy+1-vcq_iwiDFEY466=AM{fkabJqXokzXMLn5Y
z;x5c^V9-}|>@1RWaSGPf2oPG@)TD5QZQ1v`vh@b4cgxDHjdP->otd1o>*Sp8b3Q+t
z^Lg(3+nN<{aD-Ly7IS1^YJ!{r?+k_>wmimPM=x0(VSggEt1Kw&O7MXT61mI{(iga5
zHrXw2kb1CSVRrRfz8g1RNF<0F>|d(uP-HK^z4t`I3j3*!ntwlfCdJH&Tb2Ld!utKn
z98T5k%xn8)+oJ2ct<Fe4$X#&e!d9{9wp3SLMzdMVPJTJ`anGMGe|>a!>~-IE?cb}(
zXS5=FRX9GrDYM)V6Lw`cPweWx%!sfnTNN+I%$jUE=kWY}PBqUjP7OHm=H$EjX`-cz
z7G_VKE8j8grt7jyy}6c}{in{_=5L#Bp`)GkU#~6I)tC9+`IGymzFj^2PLAWx%^uo&
z7H!-)b^Uewa^rhW{3p9+-TKL6Z(Lj?H}jv#@x7tf=RB*qn|g-tcwvB-(dBnC&(n%L
zZBwFH!{Ur(I9S;2tg<KNevOuYn{xO0{i3BCXL=;6*T3=LtBrY;mh>|4UAdsgwxWhu
zhrYvg>g{U_yrUZ|gVk>Y>Ba4w*`;3^EYix|q@W}AV8v9P84ku9{6z{%`z3dYb$!yv
z=uKqUxoOcqCJ~DlR@!GasC4ptU4AR5?$cRDm%tnOFQNjcyjinW{9LMG!9~a48#ZhG
z3J%U$xn-^Wmiu!*|F#e?waAg@F@7^yC3@AV<gFax`Y(>znY}Sd{;7YaAh~$;-e!X&
zk7|>5*N?Z&FTJr(?M%U6(Q50In~yi&GTyMY_Gw7im6r#k+BeB2I-XYd44M05^6umP
zohzko*mvFx{&chQ!HeKci_(~v9+1?oVq3dbFRp#2&VtWBz1WNzW*$g(*mgLNxour8
zxAB}gPm)i+JA7A)?Z&1}Ev@UrH@yA5YSFQ0*ZwY2C^@;?_q(ZM>GKXL_PAF;x|~e~
zDX-t1YBCqU&AspGQf>|XScj(@qsnA$yx#8Y-m-;lo$I8FhyUcMUl&T>e4IBnT6CpN
z%>V1HyZBFSf1moW*>zjB_L;Mb49s7<on0u+8+*F<i-SqYTj%*Iu@T#zb<bNDSl#`&
zZJn#Ho=aq)YXaAS6+6$X@46{@G0f}@JA?D}e+<iF^D++ECv)DH{iPeoW5$@zpv-vk
z!dBb6oJaUh{_Z~@o7>3nd0MW*`-eeV`z}=%e>$mW!rY+V$ZFWtZ@>~6c(kuK)pcrv
z>w)UV1dc!f31geNXTF%UEnPmzGQ~iXdD5-RXY^8jUDl{vvg3B+_pqx5=_jRB0?!zh
zylpAvS7%(@!0WKi`SX9Kn{Dfko>@{OcxsEn2F@EQ+OKL4+%bOs`q>=I`0xa#v=c06
zR&eJ2yD@PakGsV7Yrm?5PD~apZJm1OhAOj#wsuzA!tAx%c*|!Uu}hHuuxRTqJ4X?=
z<_RJTBl4N*Cb=ZW*nHc*FgtbAA~EJ**%LvGvOA7XeaJDH<H#!4R9D_3KV#0bpR>B+
zGevaknG0J*4V$m^b}Y<(-cYKyWc|r5E31b*(R*G6efM*cGAmgtS8=fQ3u9#9an(m$
z%sC}1Z%>%e#v7Zx=~d$LGt)#%Yn0X*91xqnt6ccfhN%K~UpqzVXlKQN1R1AW=_>L{
z?@D|0CzQKENjs~KUvk^`qR5h;Lbon#6?T}*o!R>M$|b(#|92h{PJPPaym9r`?yqgx
zmt+2_&)zSa#g*!M_VdF()Bi-U=$o6cmcLoKX}dU!W0CQ`h1uz;uC`5^r)OOkeran1
d1-qWshZfFX9=}8S7Xt$WgQu&X%Q~loCIADNvzY(@

literal 0
HcmV?d00001

diff --git a/org.rodinp.handbook.feature/latex/tutorial-03.tex b/org.rodinp.handbook.feature/latex/tutorial-03.tex
index 8704d03..5f29fad 100644
--- a/org.rodinp.handbook.feature/latex/tutorial-03.tex
+++ b/org.rodinp.handbook.feature/latex/tutorial-03.tex
@@ -33,6 +33,23 @@ We cover a few examples in this chapter that should develop your ability to answ
 
 Jean-Raymond Abrial has something to say about this in his book\footnote{\url{http://www.amazon.com/Modeling-Event-B-System-Software-Engineering/dp/0521895561}}. Some of the chapters are available in the Rodin Wiki.
 
+\begin{rodin-plugin}{pror.png}{ProR Requirements}
+\index{requirements}
+\index{ProR Requirements Tool}
+\index{traceabililty}
+\index{specification}
+
+It takes some time to learn how to read formal specifications, and not all stakeholders are willing to learn it.  Further, textual requiremenets are almost always the starting point for a formal specification.  It would be nice to kep a traceability to the origianl requirements.
+
+\href{http://wiki.event-b.org/index.php/ProR}{ProR} is a tool for editing requirements.  An integration with Rodin exists, which allows a traceability between textual requirements and model elements to be established.  This shows the Event-B model elements seamless as part of the textual requirements.  The various traceability options are demonstrated in the \href{http://www.formalmind.com/en/blog/using-rmf-integrate-your-models}{Formal Mind Blog}.
+
+Further, the traces are tracked, and if the source or the target of a trace changes, a marker is set, so that the changes can be inspected and verified.
+
+Being able to set traces is not enough, if there is not a theory behind it to make it useful.  One such theory is based on the WRSPM reference model.  How this works in practice can be seen in \href{http://www.stups.uni-duesseldorf.de/w/Special:Publication/RMF_Mark_Book_Jastram_2013}{this paper}.
+
+Last, ProR is based on the ReqIF standard, which is supported by major industry tools for requirements management (like Rational DOORS or PTC integrity).  This eases the integration of Event-B into existing development processes.
+\end{rodin-plugin}
+
 \subsection{Project Setup}
 \label{tut_project_setup}
 
-- 
GitLab