| \documentclass[a4paper]{article} |
| \usepackage{zed-csp} |
| \usepackage{graphicx} |
| %\markboth{Draft}{Draft} |
| \pagestyle{myheadings} |
| \begin{document} |
| \parskip 6 pt |
| \parindent 0 pt |
| |
| \title{A CSP Model Spring Dynamic Modules (v0.1)} |
| \author{Glyn Normington} |
| \maketitle |
| % The following three commands ensure the title page is stamped as |
| % confidential without a page number. Page numbering is started at the |
| % table of contents. |
| \thispagestyle{myheadings} |
| \pagenumbering{roman} |
| \setcounter{page}{0} |
| |
| %============================================================================= |
| The aim is to model the concurrency features of Spring DM. |
| |
| \clearpage |
| \pagenumbering{roman} |
| \tableofcontents |
| |
| % Type checking hacks |
| \newcommand{\true}{true} |
| \newcommand{\false}{false} |
| \renewcommand{\empty}{\emptyset} |
| \newcommand{\ModuleDefZero}{ModuleDef_0} |
| \newcommand{\ModuleDefOne}{ModuleDef_1} |
| \newcommand{\ModuleDefTwo}{ModuleDef_2} |
| \newcommand{\ModuleDefThree}{ModuleDef_3} |
| \newcommand{\ModuleDefFour}{ModuleDef_4} |
| |
| %============================================================================= |
| %\clearpage |
| %\pagenumbering{arabic} |
| %\section{Introduction} |
| %\label{cha:intro} |
| % |
| %To do: |
| %\begin{itemize} |
| %\item |
| %\end{itemize} |
| % |
| %============================================================================= |
| \clearpage |
| \pagenumbering{arabic} |
| \section{Bundles} |
| |
| The events in this model should be just sufficient to model the interaction between bundles and Spring DM. |
| |
| We recycle bundles to avoid artificial deadlock. |
| \begin{displaymath} |
| channel~b\_started, b\_stopping: bundle \\ |
| ~\\ |
| Bundles = \\ |
| \t1 let \\ |
| \t2 Bundle(i) = b\_started.i \then b\_stopping.i \then Bundle(i) \\ |
| \t1 within \\ |
| \t2 \Interleave _{i:bundle} Bundle(i) \\ |
| \end{displaymath} |
| |
| %============================================================================= |
| \section{Service Registry} |
| \begin{displaymath} |
| channel~sr\_publish, sr\_lookup, sr\_retract: service \\ |
| ~\\ |
| ServiceRegistration(s) = sr\_publish.s \then PublishedServiceRegistration(s) \\ |
| ~\\ |
| PublishedServiceRegistration(s) = \\ |
| \t1 sr\_lookup.s \then PublishedServiceRegistration(s) \extchoice |
| sr\_retract.s \then ServiceRegistration(s) \\ |
| ~\\ |
| ServiceRegistry = \Interleave _{s : service} ServiceRegistration(s) \\ |
| \end{displaymath} |
| |
| %============================================================================= |
| \section{Application Contexts} |
| Recycle application contexts to avoid artifical deadlock, but only within a single bundle start/stop cycle. |
| \begin{displaymath} |
| channel~ac\_start, ac\_stop, ac\_refresh, ac\_close, ac\_fail, ac\_timeout: application\_context \\ |
| ~\\ |
| StopAppCtx(a) = ac\_stop.a \then AppCtx(a) \\ |
| ~\\ |
| AppCtx(a) = \\ |
| \t1 let \\ |
| \t2 Normal = ac\_refresh.a \then ServiceLookup(a, service) \\ |
| \t2 Error = ac\_fail.a \then StopAppCtx(a) \\ |
| \t1 within \\ |
| \t2 ac\_start.a \then (Normal \extchoice Error) \\ |
| \end{displaymath} |
| \begin{displaymath} |
| ServiceLookup(a, \emptyset) = ServicePublish(a, \emptyset, \emptyset) \\ |
| ~\\ |
| ServiceLookup(a, remaining) = \\ |
| \t1 let \\ |
| \t2 Timeout = ac\_timeout.a \then StopAppCtx(a) \\ |
| \t2 Lookup = (\Intchoice _{s:remaining} sr\_lookup.s \then ServiceLookup(a, remaining \setminus \set{s})) \timeout Timeout \\ |
| \t1 within \\ |
| \t2 ServicePublish(a, remaining \inter get\_services(a), \emptyset) \intchoice Lookup \\ |
| \end{displaymath} |
| \begin{displaymath} |
| ServicePublish(a, \emptyset, published) = RunningAppCtx(a, published) \\ |
| ~\\ |
| ServicePublish(a, remaining, published) =\\ |
| \t1 let \\ |
| \t2 PublishMore(s) = ServicePublish(a, remaining \setminus \set{s}, published \union \set{s}) \\ |
| \t2 Publish = \Intchoice _{s:remaining} sr\_publish.s \then PublishMore(s) \\ |
| \t1 within \\ |
| \t2 RunningAppCtx(a, published) \intchoice Publish \\ |
| \end{displaymath} |
| \begin{displaymath} |
| RunningAppCtx(a, published) = ac\_stop.a \then ac\_close.a \then ServiceTerm(a, published) \\ |
| \end{displaymath} |
| \begin{displaymath} |
| ServiceTerm(a, \emptyset) = AppCtx(a) \\ |
| ~\\ |
| ServiceTerm(a, published) = \Extchoice _{s:published} sr\_retract.s \then ServiceTerm(a, published \setminus \set{s}) \\ |
| \end{displaymath} |
| \begin{displaymath} |
| AppCtxs = \Interleave _{a:application\_context} AppCtx(a) \\ |
| \end{displaymath} |
| |
| %============================================================================= |
| \section{Bundle to application context multiplexing} |
| Multiplex bundle stopped and starting events to application context start and stop events, respectively. |
| \begin{displaymath} |
| Multiplex(i) = \\ |
| \t1 let \\ |
| \t2 ac = get\_app\_ctxs(i) \\ |
| \t2 StartAppCtxs(\emptyset) = Multiplex(i) \\ |
| \t2 StartAppCtxs(acs) = \Extchoice _{a:acs} ac\_start.a \then StartAppCtxs(acs \setminus \set{a}) \\ |
| \t2 StopAppCtxs(\emptyset) = Multiplex(i) \\ |
| \t2 StopAppCtxs(acs) = \Extchoice _{a:acs} ac\_stop.a \then StopAppCtxs(acs \setminus \set{a}) \\ |
| \t1 within \\ |
| \t2 b\_started.i \then StartAppCtxs(ac) \extchoice b\_stopping.i \then StopAppCtxs(ac) \\ |
| ~\\ |
| Multiplexer = \Interleave _{i:bundle} Multiplex(i) \\ |
| \end{displaymath} |
| %============================================================================= |
| \section{System} |
| A system comprising bundles, multiplexer, application contexts, and the service registry. |
| \begin{displaymath} |
| MultiplexedBundles = (Bundles \parallel[\set{|b\_started, b\_stopping|}] Multiplexer) \hide \\ |
| \t6 \set{|b\_started, b\_stopping|} \\ |
| ~\\ |
| EmbeddedAppCtxs = \\ |
| \t1 (AppCtxs \parallel[\set{|sr\_publish, sr\_lookup, sr\_retract|}] ServiceRegistry) \hide \\ |
| \t2 \set{|~sr\_publish, sr\_lookup, sr\_retract~|} \\ |
| ~\\ |
| System = MultiplexedBundles \parallel[\set{|~ac\_start, ac\_stop~|}] EmbeddedAppCtxs \\ |
| \end{displaymath} |
| |
| |
| \end{document} |