# Annotation of /pubs/papers/20060327_phd_topic_proposal/phdtopicpropa.tex

Commit of Ph.D. topic proposal.

 1 dashley 8 %$Header: /home/dashley/cvsrep/e3ft_gpl01/e3ft_gpl01/dtaipubs/cron/2006/phdtopicpropa/phdtopicpropa.tex,v 1.20 2006/03/27 00:10:30 dashley Exp$ 2 \documentclass[letterpaper,10pt,titlepage]{article} 3 % 4 %\pagestyle{headings} 5 % 6 \usepackage{amsmath} 7 \usepackage{amsfonts} 8 \usepackage{amssymb} 9 \usepackage[ansinew]{inputenc} 10 \usepackage[OT1]{fontenc} 11 \usepackage{graphicx} 12 % 13 \begin{document} 14 %----------------------------------------------------------------------------------- 15 \title{Ph.D. Topic Proposal} 16 \author{\vspace{2cm}\\David T. Ashley\\\texttt{dta@e3ft.com}\\\vspace{2cm}} 17 \date{\vspace*{8mm}\small{Version Control Revision: 1.20  \\ 18 Version Control Date: 2006/03/27 00:10:30  (UTC) \\ 19 RCSfile: phdtopicpropa.tex,v  \\ 20 \LaTeX{} Compilation Date: \today{}}} 21 \maketitle 22 23 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 24 % 25 \begin{abstract} 26 This document describes my Ph.D. research interests and provides 27 supporting information. The interests 28 (described in \S{}\ref{srin0}) revolve around the mathematical 29 basis of timed automata systems and code generation 30 from timed automata models. 31 \end{abstract} 32 33 \clearpage{} 34 \pagenumbering{roman} %No page number on table of contents. 35 \tableofcontents{} 36 \clearpage{} 37 \listoffigures 38 \clearpage{} 39 40 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 41 %Force the page number to 1. We don't want to number the table of contents 42 %page. 43 % 44 \setcounter{page}{1} 45 \pagenumbering{arabic} 46 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 47 48 \section{The Timed Automata Framework} 49 \label{staf0} 50 51 The framework of timed automata isn't commonplace in electrical 52 engineering, so this section provides 53 a description. 54 55 56 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 57 58 \subsection{The Framework} 59 \label{staf0:stfw0} 60 61 The formal framework of timed automata consists of systems of 62 automatons, each with discrete states, transitions, and 63 timers that can be reset to zero on transitions. 64 65 The framework includes synchronization mechanisms between automatons (i.e. 66 automatons may interact in well-defined ways)\@. Synchronization mechanisms 67 consist of soft'' synchronization mechanisms and hard'' synchronization 68 mechanisms. 69 70 \begin{itemize} 71 \item \emph{Soft} synchronization mechanisms involve one automaton having transition 72 functions that involve the discrete state or timers of another automaton. 73 \item \emph{Hard} synchronization mechanisms involve events. The semantics 74 of an event require two or more 75 automatons to make corresponding transitions at exactly the same time. 76 \end{itemize} 77 78 The details of the framework aren't especially important, 79 and there are several 80 variations on the framework\footnote{Variations include 81 substates, differences in the semantics of events, and dynamics that go beyond 82 $\dot{t} = 1$ (i.e. hybrid systems).} that don't change the essential properties. 83 84 The essential properties of the framework (that don't change with the variations) are: 85 86 \begin{itemize} 87 \item A system of timed automata that interact via synchronization 88 mechanisms can be mathematically combined into a single 89 larger automaton with a single 90 discrete state space. 91 \item There is some symbolic method of reasoning about what values 92 timers can attain in each discrete state (polytopes, DBMs, etc.). 93 \item The symbolic reasoning about timer values often allows reasoning about 94 properties of the system (reachability, liveness, etc.). 95 \end{itemize} 96 97 Timed automata are recognizeable to any embedded software engineer as 98 state machines''. A typical automotive embedded system consists of many 99 features and software components involving discrete state. For example, 100 software to control an automobile drivetrain with features like automatic 4-wheel drive 101 as well as sensor and actuator failure modes tends to have a very large discrete 102 space. 103 104 As a contrived example of a system of timed automata, consider the problem of 105 controlling a drawbridge with one motor and two limit switches so that it goes up and down 106 with period $K_D + K_U$ (Fig. \ref{fig:staf0:stfw0:000}). 107 108 \begin{figure} 109 \centering 110 \includegraphics[width=4.0in]{system01.eps} 111 \caption{Example Timed Automata System (Drawbridge Control)} 112 \label{fig:staf0:stfw0:000} 113 \end{figure} 114 115 Assume that when raising the drawbridge, it is adequate to energize the motor 116 until the limit switch $U$ closes. However, when closing the drawbridge, 117 it is necessary to energize the motor for time $K_L$ beyond 118 when the limit switch $D$ closes (the $B_{DOWNLOCK}$ state in 119 Fig. \ref{fig:staf0:stfw0:01}). 120 121 One way to design such a system is with two automata 122 (Fig. \ref{fig:staf0:stfw0:00} and Fig. \ref{fig:staf0:stfw0:01}) interacting via 123 synchronization mechnisms. 124 125 The automaton of Fig. \ref{fig:staf0:stfw0:00} alternates between two 126 states with period $K_D + K_U$. At any point in time, the state of this 127 automaton indicates whether the drawbridge should be down or up. 128 129 \begin{figure} 130 \centering 131 \includegraphics[height=2.5in]{exta01.eps} 132 \caption{Example Timed Automaton (Drawbridge Target Position Determination)} 133 \label{fig:staf0:stfw0:00} 134 \end{figure} 135 136 The automaton of Fig. \ref{fig:staf0:stfw0:01} directly 137 determines the energization of the bridge motor as a function of 138 the limit switches $D$ and $U$, the discrete state of the automaton 139 of Fig. \ref{fig:staf0:stfw0:00}, and time. 140 In the $B_{IDLE}$ state, the motor is deenergized. 141 In the $B_{UP}$ state, the motor is energized to move the 142 drawbridge up. In the $B_{DOWN}$ and $B_{DOWNLOCK}$ states, 143 the motor is energized to move the drawbridge down. 144 145 \begin{figure} 146 \centering 147 \includegraphics[width=4.6in]{exta02.eps} 148 \caption{Example Timed Automaton (Drawbridge Motor Control)} 149 \label{fig:staf0:stfw0:01} 150 \end{figure} 151 152 Mathematically, the automata of Figs. 153 \ref{fig:staf0:stfw0:00} 154 and 155 \ref{fig:staf0:stfw0:01} can be combined to give the automaton of 156 Fig. \ref{fig:staf0:stfw0:02}\@. This mathematical operation is sometimes called the 157 shuffle'' operation. 158 159 \begin{figure} 160 \centering 161 \includegraphics[width=4.6in]{exta03.eps} 162 \caption{Example Timed Automaton (Shuffle of Fig. \ref{fig:staf0:stfw0:00} and Fig. \ref{fig:staf0:stfw0:01})} 163 \label{fig:staf0:stfw0:02} 164 \end{figure} 165 166 In Fig. \ref{fig:staf0:stfw0:02}, each of the eight discrete states 167 corresponds to one discrete state from Fig. \ref{fig:staf0:stfw0:00} 168 and one discrete state from In Fig. \ref{fig:staf0:stfw0:01}. 169 The initial state $A_{D}B_{IDLE}$ corresponds to the initial state 170 from In Fig. \ref{fig:staf0:stfw0:00} paired with the initial state 171 from Fig. \ref{fig:staf0:stfw0:01}. 172 173 The noteworthy features of Fig. \ref{fig:staf0:stfw0:02} are: 174 175 \begin{itemize} 176 \item It is the result of a mathematical algorithm applied to 177 Figs. \ref{fig:staf0:stfw0:00} and \ref{fig:staf0:stfw0:01}. 178 If the underlying system consisted of more than two automata, the 179 algorithm could be applied repeatedly to generate a single automaton with 180 a single large discrete state space. 181 \item The upper bound on the number of discrete states in the shuffle 182 of two automata is the product of the number of discrete states 183 in each. Note, however, that $A_{D}B_{UP}$ and $A_{U}B_{DOWN}$ 184 don't truly'' exist. The reason is that the synchronization 185 mechanisms between the two automata ensure that these states 186 are instantly exited as soon as they are entered. Thus, a system 187 of equivalent functionality can be constructed with six discrete 188 states rather than eight. 189 \end{itemize} 190 191 Although the preceding example is contrived, it illustrates the flavor 192 of the framework and how separate automata with synchronization mechanisms can be 193 combined (and perhaps also separated'' or factored'', \S{}\ref{srin0:star0}). 194 195 It should also be apparent that tools can verify a great deal about 196 the system through symbolic manipulation. Properties that can be verified 197 include: 198 199 \begin{itemize} 200 \item \emph{Reachability:} it can be symbolically determined whether 201 or not each state is reachable (the algorithms involve determining 202 symbolically which values timers can achieve in each discrete state and 203 comparing that information against transition functions---some transitions 204 cannot ever be taken). 205 \item \emph{Liveness:} it can be symbolically determined whether the system 206 can enter a state where no inputs to the system can cause all of a 207 set of states to be reachable. 208 \end{itemize} 209 210 The example comes \emph{very} close to the way practical 211 software systems are constructed. Generally, state machines in 212 software have transition functions that involve time and the states of 213 other state machines. 214 215 216 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 217 218 \subsection{Human Tendencies} 219 \label{staf0:shtd0} 220 221 My experience in industry is that human beings do badly with the 222 design of stateful controllers. Typical tendencies: 223 224 \begin{itemize} 225 \item \textbf{Bloating of the controller state space:} 226 \;It is very common for engineers to design a controller with 227 a discrete state space that is too large. The prototypical 228 example is an engineer who finds a way to implement a purely combinational 229 function using sequential logic. 230 231 In the most humorous case (purely combinational logic implemented as 232 sequential logic), 233 the system usually behaves correctly. Serious software defects 234 most typically come about through \emph{subtle} design mistakes. A typical software defect 235 involves two or more software components with some interaction that enter 236 states such that the software can't recover. 237 \item \textbf{Inability to comprehend all possible behaviors of the system:} 238 Very stateful systems tend to be incompatible with human cognitive 239 ability. Even when the problem is well-defined and when the controller and 240 plant are operating perfectly, human beings don't do 241 well at considering every possible behavior. 242 \item \textbf{Inability to comprehend how the system may behave in the presence 243 of failures:} 244 Very stateful systems are often designed to be tolerant of certain types 245 of sensor and actuator failures (usually in the sense that the failures will 246 be detected and the system will employ a different algorithm to operate without 247 a specific sensor or actuator)\@. Such fault detection and tolerance 248 normally complicates the software design substantially. 249 250 However, even without designed-in fault tolerance, there is the need to 251 design controllers to tolerate the faults that can occur in any practical system. 252 Specific scenarios that must be tolerated: 253 254 \begin{itemize} 255 \item Spurious reset of the controller (which will normally reset the controller 256 to its initial state but leave the plant undisturbed). (This directly implies that 257 the system must recover from the initial state of the controller combined with 258 any state of the plant.) 259 \item State upset of the controller (due to electrical noise, internal software errors, 260 etc.). (This directly implies that the system must recover from any state of 261 the controller combined with any state of the plant.) 262 \end{itemize} 263 264 Except in simple cases, human beings don't have the cognitive capacity to consider 265 all possible behaviors when both the controller and the plant may start in any state. 266 \end{itemize} 267 268 One example that comes to mind from product development is an automobile transfer case controller 269 where it was discovered that if the electrical connector was removed, the transfer case mechanical 270 components repositioned, and the electrical connection restored; the controller would not 271 recover into normal operation. Human beings are not good at mentally exploring all possibilities, and even 272 a disciplined manual process can't be used because the combinations sometimes number in the thousands 273 or more. A mathematical framework and tool support are required. 274 275 276 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 277 278 \subsection{Code Generation} 279 \label{staf0:scgn0} 280 281 In most engineering environments, software is generated 282 from software designs that involve timed automata. (Some of the techniques 283 used to create compact code are described in \S{}\ref{sfrr0}.) 284 285 For some types of systems, there has been success in using 286 existing tools to generate code directly from the software design 287 (using tool chains from \emph{The Math Works} or \emph{I-Logix}). It is, 288 however, known from experience that a clever human programmer can generate 289 more compact code than any existing tool; so code generation tools have 290 not penetrated cost-sensitive automotive products involving 32K of FLASH or less. 291 292 There are two primary arguments against manual generation of code: 293 294 \begin{itemize} 295 \item Code is redundant with respect to a software design. 296 In general, it does not make economic sense to maintain redundant 297 information using human labor. 298 \item The act of optimizing implementations typically destroys the 299 clear relationship between design and code. Furthermore, changes 300 to the design---sometimes even small ones---can invalidate the 301 mathematical basis for certain optimizations. Optimized code becomes 302 unmaintainable. It would be more economical to evaluate the viability 303 of optimizations and to generate code using software tools (rather than 304 human labor). 305 \end{itemize} 306 307 308 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 309 310 \subsection{Formal Verification of Properties} 311 \label{staf0:svpr0} 312 313 Typical design tools provide simulation capability, and there is a large 314 body of theory and best practice about how to design test cases based on 315 a stateful design. 316 317 Still, the following problems remain: 318 319 \begin{itemize} 320 \item Systems with a large discrete state space elude human 321 understanding. 322 \item It is very laborious to test systems with a large discrete 323 state space. 324 \item It isn't possible to fully test systems with a large 325 discrete state space. 326 \item It is possible (and common) to make a good faith effort at 327 comprehensively testing systems but still to overlook 328 unacceptable behavior. 329 \end{itemize} 330 331 \emph{Simulation and testing are not enough.} For complex safety-critical 332 systems, simulation and testing do not provide enough assurance about the 333 behavior of the system. 334 335 Formal verification of properties would involve making mathematical assertions 336 about how the system must and must not behave, and then allowing 337 tools to verify the properties. 338 339 Possible types of properties: 340 341 \begin{itemize} 342 \item \emph{Required behavior:} 343 For example: \emph{When the brake pedal switch is closed, 344 the brake lights must always come on within 200ms.} 345 \item \emph{Required absence of behavior:} 346 For example: \emph{The airbags can never deploy without at least one 347 body deformation sensor indicating body deformation.} 348 \item \emph{Liveness:} 349 For example: \emph{A certain set of states is always reachable by manipulating certain 350 inputs.} 351 \end{itemize} 352 353 The only tool I'm aware of that allows formal verification of properties 354 is UPPAAL. However, the modeling framework of 355 UPPAAL isn't rich enough to support practical embedded systems.\footnote{The 356 tool chains from \emph{The Math Works} and \emph{I-Logix} don't attempt 357 formal verification at all.} 358 359 I would tend to view formal verification of properties as a last line of defense 360 against egregious software defects (i.e. as a practice that cannot stand alone)\@. 361 Formal verification should be combined with all other known 362 best practices. 363 364 365 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 366 367 \section{FLASH/ROM Reduction Techniques} 368 \label{sfrr0} 369 370 In this section, I mention some of the FLASH/ROM reduction techniques 371 used by human programmers. Important points: 372 373 \begin{itemize} 374 \item All of the techniques have a mathematical basis. 375 \item The techniques are complex to apply and best carried out by tools. 376 \item The mathematical basis of the techniques is non-trivial. There are 377 many unexplored corners. 378 \item The techniques distort the correspondence (i.e. the resemblance) 379 between design and code, and make code unmaintainable (it would be 380 better only to generate code from designs and never to maintain 381 code directly). 382 \end{itemize} 383 384 The list of techniques presented is not exhaustive (far more techniques 385 exist). 386 387 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 388 389 \subsection{General Paradigm of Software Construction for Small Microcontrollers} 390 \label{sfrr0:sgsc0} 391 392 This discussion is confined entirely to systems where a stateful design is 393 implemented directly as code (with no tabulation or compression of the design). 394 Other paradigms are possible. For example, at least one tool on the market implements 395 stateful designs as state transition tables that are evaluated at runtime by 396 a table interpreter. My experience with these types of systems is that there 397 is always a real-time performance penalty (but certainly not always a 398 FLASH penalty). My research interests do also include event-driven systems 399 and systems where the design is not implemented directly as code; but these 400 systems are not mentioned for brevity. 401 402 The most common paradigm for small systems is \emph{a collection of cooperating 403 timed automatons}''. The most typical abstraction of these systems is a data-flow 404 diagram, with RAM variables (i.e. global variables) used as the interfaces. 405 406 There is a body of theory and best practice about what separates good software designs 407 and implementations from bad (Parnas and the classic coupling and cohesion spectrums 408 come to mind). However, in small systems, it simply isn't possible to 409 implement the systems using classic good'' programming practice---formal parameters, 410 pointer dereferencing, and access to variables in stack frames all bloat 411 FLASH size under the weak instruction sets typical of small microcontrollers. 412 413 It is helpful to take a step back and consider the possibility that global variables 414 (the second-strongest form of coupling in the classic coupling spectrum) aren't 415 inherently harmful; but rather that it is the way in which global variables are 416 typically used that causes harm. The harmful aspects of global variables 417 seem to be: 418 419 \begin{itemize} 420 \item If global variables are tested \emph{and assigned} in more than place, 421 the variable actually becomes an automaton and adds to the 422 state space of the system. 423 \item Global variables lead to unrestrained connectivity: \emph{any} 424 software component can access the variables. Additionally, 425 state is not shed'' as functions return (as happens with formal 426 parameters and local variables)\@. This leads to connectivity 427 that often skips levels of the calling tree (making it very 428 difficult to understand the software). 429 \end{itemize} 430 431 Small systems often have design rules to mitigate the harmful aspects of 432 global variables. The design rules tend to involve these restrictions: 433 434 \begin{itemize} 435 \item A global variable used as an interface can be assigned by only one 436 software component (a 1-writer, $n$-reader restriction). 437 \item A global variable used as an interface has its readers/writers 438 represented in design documentation (so that the connectivity 439 created by the global variable isn't accidental or unrestrained). 440 \end{itemize} 441 442 The design rules typically also include provisions for global variables 443 used as interfaces that are tested and assigned by more than one software 444 component (i.e. interface automatons). The simplest example of such an 445 interface is a semaphore that is 446 set \emph{T} by one software component and tested and set \emph{F} by 447 another software component, but the design rules are far more general. 448 449 Note that tools can be used to allow a system to be phrased in a way 450 consistent with the traditional coupling spectrum but implemented 451 efficiently for small microcontrollers. For example, some compilers 452 are able to analyze the calling tree and place variables of storage 453 class \emph{automatic} into statically overlaid\footnote{Statically overlaid 454 based on the calling tree: one function's automatic variables can be overlaid 455 with another only if an analysis of the calling tree determines that 456 the two functions cannot be active at the same time.} areas of memory rather than 457 in a stack frame. Similar tool support could be developed for the notion of 458 \emph{automatic} bitfields and to restrain the connectivity introduced 459 by global variables to be consistent with the product design. 460 461 462 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 463 464 \subsection{Near versus Far (Addressing Modes)} 465 \label{sfrr0:snvf0} 466 467 Most small microcontrollers (TMS370C8, 68HC05, etc.) have two 468 non-indexed addressing modes, typically called \emph{direct} and 469 \emph{extended}. Instructions using the direct addressing mode typically 470 have the address encoded as a single byte, and can address only locations 471 \$00 through \$FF\@. Instructions using the extended addressing mode 472 typically have the address encoded as two bytes, and can address 473 locations \$0000 through \$FFFF. 474 475 For lack of better nomenclature, I'll call the RAM locations that can be addressed 476 using short instructions \emph{near} RAM, and the RAM locations that require 477 long instructions \emph{far} RAM. 478 479 When fixed RAM locations are used as interfaces (\S{}\ref{sfrr0:sgsc0}), 480 one can save substantial FLASH by allocating the variables that are 481 referenced most often throughout the software into near RAM. 482 483 In automotive software, variables such as gearshift position and vehicle speed 484 are typically referenced many times throughout FLASH. Most programmers 485 would automatically place these into near RAM. 486 487 However, for most variables, it isn't obvious whether these should be placed 488 into near or far RAM. 489 490 Software developers often write small utility programs to scan all software 491 modules to determine the number of references to each variable. This information 492 is then used to allocate the variables with the most references into near RAM. 493 494 The FLASH savings from using this technique is typically large. As an example, 495 assume there are ten variables each referenced 50 times throughout the software. 496 The savings of placing these variables into near RAM versus far RAM is 497 typically about $50 \times 10 = 500$ bytes of FLASH (more than 1\% of a 498 32K FLASH). 499 500 501 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 502 503 \subsection{Treatment of Time} 504 \label{sfrr0:stot0} 505 506 The way that time is measured is usually the single most important decision 507 in a small embedded system. Typically, many software components have to 508 measure time intervals, so a suboptimal decision about the mechanisms 509 greatly increases FLASH consumption. 510 511 The best mechanism known is to arrange all software timers into 512 binary decades and to decrement the timers en masse 513 (Fig. \ref{fig:sfrr0:stot0:00}). 514 515 \begin{figure} 516 \begin{small} 517 \begin{verbatim} 518 unsigned char modulo_counter; 519 unsigned char timers_modulo_1[MOD1_COUNT]; 520 unsigned char timers_modulo_2[MOD2_COUNT]; 521 unsigned char timers_modulo_4[MOD4_COUNT]; 522 523 void decrement_timers(void) 524 { 525 int i; 526 527 modulo_counter++; 528 529 for (i=0; i