LayoutEngine Implementation

doc/statechart-paper/.svn/entries

@@ -0,0 +1,96 @@
+10
+
+dir
+199
+file:///home/sujit/myrepository/statechart-paper
+file:///home/sujit/myrepository
+
+
+
+2017-04-05T14:28:33.500582Z
+199
+sujit
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+31053f9d-af06-4b75-a4bf-4fd01afd5eef
+
+spec-with-statecharts.tex
+file
+203
+
+
+
+2017-04-07T14:20:38.847368Z
+9767575063d7c6e31272175f710e2a97
+2017-04-07T14:21:25.490895Z
+203
+sujit
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+14570
+
+syntax.ml
+file
+202
+
+
+
+2017-04-05T14:29:50.125553Z
+4b3950e379f8ca8f7ceebc8c2c208ac0
+2017-04-07T13:58:17.529844Z
+202
+sujit
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+1363
+

doc/statechart-paper/.svn/text-base/spec-with-statecharts.tex.svn-base

@@ -0,0 +1,178 @@
+\documentclass[12pt,a4paper]{article}
+\usepackage{algorithm}
+\usepackage{algpseudocode}
+\usepackage{listings}
+\usepackage{marvosym}
+\usepackage{wasysym}
+\usepackage{marvosym}
+\usepackage{xcolor}
+\usepackage{graphicx}
+\usepackage{tikz}
+\usepackage{framed}
+%\usepackage{amsmath,bm,times}
+\usetikzlibrary{positioning,shapes,arrows,backgrounds,fit, calc, shadows}
+
+\author{Karthika Venkatesan, IIITB \\ Sujit Kumar Chakrabarti, IIITB }
+\title{Formal Specification with Statecharts}
+\date{}
+\begin{document}
+\definecolor{lightblue}{rgb}{0.8,0.93,1.0} % color values Red, Green, Blue
+\definecolor{Blue}{rgb}{0,0,1.0} % color values Red, Green, Blue
+\definecolor{Red}{rgb}{1,0,0} % color values Red, Green, Blue
+\definecolor{Purple}{rgb}{0.5,0,0.5}
+\definecolor{Pink}{rgb}{0.7,0,0.2}
+
+\newcommand{\highlight}[1]{{\color{Red}(#1)}}
+\newcommand{\comment}[1]{{\color{Blue}#1}}
+
+
+\lstset{
+	language = ML,
+	basicstyle = \ttfamily,
+	stringstyle = \ttfamily,
+	keywordstyle=\color{Blue}\bfseries,
+	identifierstyle=\color{Pink},
+	frameround=tttt,
+%	numbers=left
+	showstringspaces=false
+}
+
+\maketitle
+\abstract{
+UML Statecharts have enjoyed widespread popularity in software development community as a design and specification notation. It has primarily been employed for specification of object life-cycles. In this paper, we explore the option of using Statecharts in specifying GUI interactions, typically in web applications. A notation like Statechart is very apt to be used as a formal specification language, provided the following features: Firstly, it should have well-defined semantics, so that specifications written in it can not be inherently ambiguous. Secondly, it should have tool support for automatic detection of specification bugs.
+In this work, we present enhancements and customisations to the Statechart syntax and semantics for specification of modern web applications. We also demonstrate how automatic detection of specification bugs can be performed through well-known model-checking and program analysis. We have used our specification approach in specifying a number of web applications. Our approach enabled early detection of several specification bugs and hence facilitated higher quality specification.
+}
+
+\section{Introduction}
+Statechart was proposed a visual formalism for specification of complex systems (\comment{cite Harel}). In particular, the `system' here is an object with a complex life-cycle going through a finite number of discrete \emph{states}. The notation has enjoyed a wide acceptance in software engineering community. It has been a part of the UML suite for modelling object oriented system.
+
+Application of Statecharts as a specification notation for web-based systems was explored in (\comment{cite Ricca-Tonella paper}). Features of web-based systems have evolved significantly since the time of this paper. Predominantly plain HTML forms have given place to highly interactive user-interfaces, e.g. tabbed panels, with rich client side validations as well as AJAX which permits partial page updates via asynchronous server interactions. This calls for a further look at how Statechart notation could be adapted to allow specification of richly featured modern web applications.
+
+Another angle to look at is the growing complexity of web applications. This calls for increased levels of automation in engineering these systems, in particular, requirement analysis and verification. To achieve this goal, it is more important for specification formalisms to have a formally defined semantics,  than to have rich syntactic features. A formal specification language would open doors to a variety of automated approaches to analysis, design, generation of both code and tests for modern web based systems.
+
+Contributions of this work include:
+\begin{enumerate}
+	\item Syntactic and semantic adaptation of Statechart notation for formal specification of GUI intensive applications, typically web applications
+	\item Illustration of specification defects possible in specification written using this notation
+	\item Static analysis methods to detect the above defects automatically.
+\end{enumerate}
+
+\section{Motivating Examples}
+
+\section{Statechart Language}
+Statechart provides a pictorial notation to describe the life-cycle of a system, usually object-oriented. It is an adaptation of the classical finite state automation with enhancement like hierarchical states, concurrent states, action language, communication etc., all aimed to increase its expressive power as a specification language of industrial strength software systems. 
+
+Statechart has been used widely in industry and academia as a part of various UML modelling tools [\comment{Rational Rose, Rhapsody, Telelogic, Statemate, Stateflow}]. In all industrial tools, the explicitly specified semantics of the language, if at all given, are semi-formal to the best of our knowledge. There has been a lot of research in formal specification of semantics for Statechart(-like) languages [\comment{J. Rushby paper in FASE'04 on Stateflow operational semantics etc.}]. They mostly target specific subsets of the Statechart language. We take a similar approach, defining formal syntax and semantics of the Statechart language for parts which we have found useful in formal specification of web applications. Mapping various existing features of the Statechart language to specification use-cases and formulating their formal description and building verification support for the same is a part of our ongoing research agenda.
+
+\subsection{Syntax}
+\begin{scriptsize}
+\lstinputlisting[frame=single]{syntax.ml}
+\end{scriptsize}
+
+Statechart specifications can be partitioned into their core Statechart part, and the trigger/guard/action part, typically abbreviated as the action part. The core Statechart part of the specification gives the pictorial form and finite-state nature to the specification. The action part, essentially comprised of code fragments in an appropriate imperative programming language, adds arbitrary expressiveness to the Statechart, allowing it to be infinite state in reality. In our adaptation, we have not made any modification to the core Statechart language w.r.t. Harel's notation, except -- for the time being -- postponing the treatment of some of its advanced features. However, we have provided more detailed specification of the action language part, some of them in variance with existing norms. These specifications have been accommodated to align the notation more closely to the needs of specifying GUI intensive applications in general, and web apps in particular.
+
+
+The salient points of our syntax are:
+\begin{enumerate}
+	\item \emph{Set theoretic operations.}
+	\item \emph{Local variables.}
+	\item \emph{Input and output variables of states}
+\end{enumerate}
+
+Some of the features which we retain are:
+\begin{enumerate}
+	\item Hierarchy
+	\item triggers/guards/actions
+	\item History states
+\end{enumerate}
+The important elements of Statechart which we have not considered so far are:
+\begin{enumerate}
+	\item And states
+\end{enumerate}
+\subsection{Semantics}
+As mentioned earlier, our emphasis has been on the specification of the action language. Our action language has the following semantic features.
+\begin{enumerate}
+	\item \emph{Lexical scope.} Events and variables declared in a state are visible within it, including the substates. Internal bindings shadow the external bindings.
+	\item Action on a transition are allowed to use local events and variables of the source state and define any variables of the destination state. This feature allows data-flow between successively visited states without recourse to global variables.
+\end{enumerate}
+
+\section{Specification Bugs} \label{s:sb}
+Like programs, requirement specifications are subject to faults \footnote{For our discussion, we use \emph{faults}, \emph{defects} and \emph{bugs} as synonyms.}. One of the most important goals of using formal methods is to detect such bugs automatically. Requirement bugs can be further classified as \emph{implicit} and \emph{explicit}.
+
+Implicit bugs are violations of universal properties. In programming, universal properties abound. Examples of violations of universal properties are accessing undefined variables, null-pointer dereferencing etc. Such bugs would most likely lead to catastrophic failures, like a program crash. Hence, modern compilers come with built-in support to detect many of these errors; programmers do not need to specify them explicitly. Such analysis is often based on static program analysis methods.
+
+Explicit bugs are violations of properties explicitly stated by the programmer, often arising out of the business domain, often specific to the system being modelled. For example, for a banking software, the \lstinline@balance@ attribute of a \lstinline@BankAccount@ class may never be allowed to hold a negative value. Such properties need additional analysis typically based on model-checking or theorem proving technology. 
+
+We have encountered a number of requirement bugs that could occur in a Statechart specification model which could be classified as implicit and explicit, in a sense very similar to the above. And interestingly, it turns out that the verification technologies applicable in detection of these bugs also correspond to the above: program analysis for implicit bugs, and model checking and theorem proving for explicit bugs.
+
+Further subsection of this section present some of the properties -- both implicit and explicit -- which could get violated in a specification leading to requirement bugs.  In section~\ref{s:ver}, we explain how they can be detected using static analysis techniques.
+
+\subsection{Undefined Variable Access}
+\begin{figure}
+\caption{Undefined variable}
+\label{f:undefined}
+\end{figure}
+
+Consider the Statechart fragment shown in figure~\ref{f:undefined}. On running static analysis on this model, several warnings are flagged, e.g. \lstinline@roomNumber@ for a student may turn out to be \lstinline@nil@ in a number of expressions where it is used. At several places, this corresponds to a serious flaw in the specification model. Room allocation can be done in two ways: either by first selecting a student and then going to the room allocation, or by first selecting the room and then going to the student selection. Once this process is completed, the composite state \lstinline@AllocateRoom@ terminates. Here, it is possible to complete the room allocation without actually completing the process. 
+
+\subsection{Non-Determinism}
+Statechart permits non-determinism. For instance, when multiple outgoing transitions from the current state are enabled simultaneously, the system must make a non-deterministic choice between them. Different flavours resolve non-determinism in different ways (\comment{cite various Statechart semantics papers}).
+
+Non-determinism is an instance of incompleteness in specification. Whether it is desired in the specification or not depends on the specific case. In any case, it would be desirable to be able to detect their presence automatically. For any configuration, the set of \emph{conflicting outgoing transitions} is nothing but the set of the outgoing transitions from all its states. To statically detect non-determinism, we need to check if for any given configuration, any two conflicting outgoing transitions can get enabled simultaneously.
+
+
+\subsection{Stuck Specification}
+Another problem is that of \emph{stuckness}: when there is no way left for the system to exit a particular configuration. Consider the simple Statechart fragement in figure~\ref{f:stuck}
+
+\begin{figure}[H]
+\resizebox{0.75\textwidth}{!}{%
+\begin{tikzpicture}[auto,
+    ->,
+  %  shorten >=2pt,
+    >=stealth,
+    node distance=1.5cm,
+    init/.style={%
+      circle, thick, fill=black
+    },
+    inv/.style={%
+      rectangle,draw=black, very thin, dashed,align=left,font=\scriptsize,
+      text ragged, minimum height=2em, minimum width=2em, inner sep=6pt
+    },
+    st/.style={%
+      rectangle, rounded corners=1.5mm, draw=black, thick, fill=lightblue, drop shadow,align=center,
+      text ragged, minimum height=2em, minimum width=2em, inner sep=6pt
+    },
+    tl/.style={%
+      -latex,draw=black, very thick
+    }
+  ]
+    \node[init] (s0)                {};
+    \node[st]  (s1) [right = of s0] {$s_1$: };
+
+    \draw[tl] (s0) to node[inv, above left]{$t_1$: \_/\_/$x \gets 0$} (s1);
+    \draw[tl, loop above] (s1) to node[inv, above]{$t_2$: \_/\_/$x \gets x+1$} (s1);
+    \draw[tl] (s1.east) -- node[inv, above right]{$t_3$: \_/$x<0$/\_} ++(0:2cm);
+
+  \end{tikzpicture}
+}
+
+\caption{Stuck specification: The system can not exit $s_1$}
+\label{f:stuck}
+\end{figure}
+
+\subsection{Violation of External Specifications}
+Based on the specific domain, there may be any number of additional constraints which we may want our specification to follow. 
+
+
+\section{Verification} \label{s:ver}
+In this section, we outline a number of analyses that can be used to detect the specification bugs presented in section~\ref{s:sb}.
+
+\section{Conclusion and Future Work}
+
+
+Concurrent states (And states) are a very important feature of Statechart notation which we have not considered so far. We realise that it is very relevant for specification of web applications which themselves have a large amount of concurrency built in. In the next stage of our research, we are working on incorporating concurrency into our adaptation of Statecharts. This feature -- apart from adding expressiveness -- will also make a number of additional specification bugs possible. Our next effort will be to augment our verification tool set for automatic detection of the above bugs.
+
+Wherever there was a translation required for preparing an input to a verification tool, it was performed manually. This is tedious and error prone. There exists a wealth of prior work in this direction (\comment{cite Translation of Statechart to Model Checking}). We are currently in the process of implementing some of these translators, so that the translation can be automated.
+
+In this paper, we have focused on static verification techniques. However, Statechart specifications are an excellent starting point for automated test generation. In our earlier work, we have reported an end-to-end technique to generate test cases for web applications from Statechart specification (\comment{our ModSym 2016 paper}). With addition of further features to the Statechart notation, it will be necessary to extend this test generation method to accommodate these.
+\end{document}

doc/statechart-paper/.svn/text-base/syntax.ml.svn-base

@@ -0,0 +1,51 @@
+type statechart =
+  state      *    (* initial state *)
+  state list *    (* other states *)
+  transition list (* transitions *)
+
+type state =
+    AtomicState of
+      name *  (* State name *)
+    | block * (* Entry actions *)
+    | block   (* Exit actions *) 
+  | NonAtomicState of statechart
+  | ShallowHistory
+  | DeepHistory
+  | Branch
+
+type transition = Transition of
+    id * (* source state name *)
+    id * (* destination state name *)
+    expr  * (* trigger *)
+    expr  * (* guard  *)
+    block   (* action *)
+
+block = stmt list (* statements *)
+
+stmt = Assignment of 
+        expr * (* LHS *)
+        expr   (* RHS *)
+  | Expr of expr (* independent expressions like 
+    arithmetic expressions or function calls *)
+  | Return of expr (* Returned value *)
+  | If of expr  * (* boolean condition *)
+          block * (* then block *)
+          block   (* else block *)
+  | Loop of expr * (* boolean condition *)
+            block  (* loop body *)
+
+expr =
+    BinaryExpr of expr   * (* LHS *)
+                  binop * (* Operator *)
+                  expr     (* RHS *)
+  | UnaryExpr of unaryop * (* Unary operator *)
+                 expr
+  | FunctionCall of expr * (* Function *)
+                    expr list (* actual parameters *)
+  | Id of string
+  | string_literal of string
+  | num_const of string
+  | PHI (* empty set *)
+  | Set of expr list
+
+

doc/statechart-paper/spec-with-statecharts.aux

@@ -0,0 +1,20 @@
+\relax 
+\@writefile{toc}{\contentsline {section}{\numberline {1}Introduction}{1}}
+\@writefile{toc}{\contentsline {section}{\numberline {2}Motivating Examples}{2}}
+\@writefile{toc}{\contentsline {section}{\numberline {3}Statechart Language}{2}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {3.1}Syntax}{3}}
+\@writefile{lol}{\contentsline {lstlisting}{syntax.ml}{3}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {3.2}Semantics}{4}}
+\@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces Undefined variable}}{5}}
+\newlabel{f:undefined}{{1}{5}}
+\@writefile{toc}{\contentsline {section}{\numberline {4}Specification Bugs}{5}}
+\newlabel{s:sb}{{4}{5}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {4.1}Undefined Variable Access}{5}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {4.2}Non-Determinism}{6}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {4.3}Stuck Specification}{6}}
+\@writefile{lof}{\contentsline {figure}{\numberline {2}{\ignorespaces Stuck specification: The system can not exit $s_1$}}{6}}
+\newlabel{f:stuck}{{2}{6}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {4.4}Violation of External Specifications}{6}}
+\@writefile{toc}{\contentsline {section}{\numberline {5}Verification}{7}}
+\newlabel{s:ver}{{5}{7}}
+\@writefile{toc}{\contentsline {section}{\numberline {6}Conclusion and Future Work}{7}}