diff --git a/Lectures/L29_IntroductionToVerification/IntroductionToVerification.tex b/Lectures/L29_IntroductionToVerification/IntroductionToVerification.tex index c3ff9046ee257cd87738ce27afbc0910451f54d5..b1c430e706445fde25e6720b69117213a4957ac3 100755 --- a/Lectures/L29_IntroductionToVerification/IntroductionToVerification.tex +++ b/Lectures/L29_IntroductionToVerification/IntroductionToVerification.tex @@ -481,35 +481,4 @@ Avoids potential ArrayIndexOutOfBoundsException Exception %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\begin{frame} -\frametitle{Does our Engineering Analogy Fail?} - -\begin{itemize} - -\item \structure{If a bridge can hold 512 kN, can it hold 499 kN?} -\item \structure{If our software works for the input 512, will it work for 499?} - -\end{itemize} - -\end{frame} - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -\begin{frame} -\frametitle{Verification in Engineering} - -\begin{itemize} - -\item Example of bridge design -\item One test assures infinite correct situations -\item In software a small change in the input may result in significantly different behaviour -\item There are also chaotic systems in nature, but products of engineering - design are usually stable and well-behaved -% consider the examples of weather, bifurcation in engineering, chaos theory for traffic, etc. -\end{itemize} - -\end{frame} - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \end{document} \ No newline at end of file diff --git a/Lectures/L30_IntroToVerificationContd/IntroToVerificationContd.pdf b/Lectures/L30_IntroToVerificationContd/IntroToVerificationContd.pdf index 8c05df696dc54bafdf00fa406a22be4a4e50bae3..2b706f12aaee9a8faffafa27f610d3969b2f16ec 100644 Binary files a/Lectures/L30_IntroToVerificationContd/IntroToVerificationContd.pdf and b/Lectures/L30_IntroToVerificationContd/IntroToVerificationContd.pdf differ diff --git a/Lectures/L30_IntroToVerificationContd/IntroToVerificationContd.tex b/Lectures/L30_IntroToVerificationContd/IntroToVerificationContd.tex index fab2d0f9e658b7b2cae2bb772a1200dd8b61ecb9..06c8ba13cac6a88da2a0a8965695caf273c07709 100755 --- a/Lectures/L30_IntroToVerificationContd/IntroToVerificationContd.tex +++ b/Lectures/L30_IntroToVerificationContd/IntroToVerificationContd.tex @@ -29,7 +29,7 @@ \mode<presentation>{} \input{../def-beamer} -\Drafttrue +\Draftfalse \newcommand{\topicTitle}{30 Introduction to Verification Continued (Ch.\ 6)} \ifDraft @@ -73,17 +73,20 @@ TBD { \begin{itemize} -\item A3 deadlines +\item A3 \begin{itemize} -\item Part 2 - Code: due 11:59 pm Mar 20 -\item {Part 1 spec available in repo} +\item Part 2 - Code: due 11:59 pm Mar 26 \end{itemize} \item A4 \bi -\item Now available in our repo -\item Your own design and specification -\item Due April 3 at 11:59 pm +\item Due April 9 at 11:59 pm +\item Might be tempted to write code first +\bi +\item Recommend starting with syntax of + module(s), state variables +\item Maybe program a little before semantics part +\ei \ei \end{itemize} @@ -94,6 +97,35 @@ TBD %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\begin{frame} +\frametitle{Properties of Verification} + +\begin{itemize} + +\item May not be binary (OK, not OK) +\begin{itemize} +\item Severity of defect is important +\item Some defects may be tolerated +\item Our goal is typically acceptable reliability, not correctness +\end{itemize} +\item May be subjective or objective - for instance, usability, generic level of + maintainability or portability +\bi +\item \structure{How might we make usability objective?} +\ei +\item Even implicit qualities should be verified +\begin{itemize} +\item Because requirements are often incomplete +\item For instance robustness, maintainability, performance +\end{itemize} +\item \structure{What is better than implicitly specified + qualities?} % explicit! +\end{itemize} + +\end{frame} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \begin{frame} \frametitle{Approaches to Verification} @@ -540,6 +572,15 @@ validity %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\begin{frame} +\frametitle{Quality Testing: Installability} +\begin{itemize} +\item \structure{How might you test installability?} %virtual machines, docker +\end{itemize} +\end{frame} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \begin{frame} \frametitle{Fault Testing} \begin{itemize}