\documentclass[12pt]{article} \usepackage[top=1in,bottom=1in,left=1in,right=1in]{geometry} \usepackage{alltt} \usepackage{array} \usepackage{graphicx} \usepackage{tabularx} \usepackage{verbatim} \usepackage{setspace} \usepackage{listings} \usepackage{amssymb,amsmath, amsthm}

\title{SOEN331: Introduction to Formal Methods\\for Software Engineering\\ Assignment 1 on extended finite state machines} \author{Author's name} \date{\today}

\begin{document} \begin{spacing}{1.5}

\maketitle

\section{Metro passageway formal specification}

oindent The EFSM of the metro passageway is the tuple $S = (Q, \Sigma_1, \Sigma_2, q_0, V, \Lambda)$, where\\

oindent $Q = \{locked, unlocked\}$\\ oindent $\Sigma_1 = \{request~entry, pass\}$\\ oindent $\Sigma_2 = \{lock, unlock, beep\}$\\ oindent $q_0: locked$\\ oindent $V: ticket = \{valid, invalid\}$\\ oindent $\Lambda$: Transition specifications\\ \indent 1. $ ightarrow locked$\\ \indent 2. $locked \xrightarrow {\text { request entry [ticket is valid] / (unlock ; beep)}} unlocked$\\ \indent 3. $unlocked \xrightarrow {\text { pass / lock}} locked$\\

oindent The UML state diagram is shown in Figure~ ef{fig:metro-fig}.

ewpage

\section{UML state diagrams}

\begin{figure}[h!] \centering \includegraphics[width=0.8\textwidth]{./figures/eps/metro.eps} \caption{Metro.} \label{fig:metro-fig} \end{figure}

\end{spacing} \end{document}

%% ============================================================================= %% %% CONCORDIA UNIVERSITY %% Department of Computer Science and Software Engineering %% SOEN 331-W: Assingment 1 %% Winter term, 2019 %% Date submitted: February 11, 2019 %% %% Authors: %% %% name1, id1, email1 %% name2, id2, email2 %% ... %% %% ============================================================================= %% ============================================================================= %% %% Facts %% %% ============================================================================= %% ============================================================================= %% %% Rules %% %% ============================================================================= %% eof.

1 Metro passageway formal specification The EFSM of the metro psageway is the tuple S-Q. . 2.RxV, A), where -(locked, unlocked .-{request entry. Pass} 9s : locked V:ticket (valid,inealid ATranstion specifications -locked unlocked 3, unlockedPlocked The UML state diagr am is shown in Figure 1 2 UML state diagrams metro passageway equest entry [tcket is valid]/(unloc:beep) locked unlocked pass lock 3 System description The system in discussion controls and maintains the temperature inside some room. The system uses an electrical furnace in order to build up a desired temperature with respect to the current time, set by a user. Once that temperature is reached, the furnace goes off and a fan is activated which will distribute hot air throughout the ro Furnace and fan are never both activated at the same time. The system, initially idle, can be configured for setting the desired temperature within time periods in the form of triplets, i.e. time-fron, tine-to, deaired-temperature. During configuration a user can set as many triplets as they wish, and one triplet may override another with identical data. Upon entering configuration mode, the system will produce a beep sound, and a led light will switch on and stay on as long as the syste s under configuration. Once a user has completed their entries of desired temperature(s), they can indicate the successful completion of configuration, thus letting the system get back to the During configuration, the system allows the user to cancel the current mode in which case the system gets back to the initial idle mode while producing a prolonged beep sound. Triplets that are entered prior to canellation are still registered and considered. Additionally, during configuration a timer is active which, after an inactivity for 1 minute, will cause the system to become idle. Once idle, the system goes into the following cycle which repeats every 2 minutes: It will read the current time and, based on its configuration, it will subsequently determine what is the desired temperature. The system will read the currnt room temperature, and if it is not less than the desired temperature, then it will do nothing, but to repeat the cycle. However if the current temperature is less than one degree lower than the desired temperature, then the system turns the furnace on to build up the desired temperature. During warming up, the furnace remains on, and the system goes into the following cycle which repeats every 3 minutes: It reads in the temperature within the furnace and if it less than a degree higher than the desired temperature, then it will do nothing, but to repeat the cycle. When the furnace temperature reaches a degree higher than the desired temperature, then the system goes back to being idle while turning on the fan in order to blow hot air into the room while at the same time producing a "click" sound. The system allows a user to interrupt warming up in order to perform configuration (as discussed above). The furnace cannot be on during system configuration. When idle, the system can be shut off. When the system is off, both fan and furnace must be switched off. 1 Metro passageway formal specification The EFSM of the metro psageway is the tuple S-Q. . 2.RxV, A), where -(locked, unlocked .-{request entry. Pass} 9s : locked V:ticket (valid,inealid ATranstion specifications -locked unlocked 3, unlockedPlocked The UML state diagr am is shown in Figure 1 2 UML state diagrams metro passageway equest entry [tcket is valid]/(unloc:beep) locked unlocked pass lock 3 System description The system in discussion controls and maintains the temperature inside some room. The system uses an electrical furnace in order to build up a desired temperature with respect to the current time, set by a user. Once that temperature is reached, the furnace goes off and a fan is activated which will distribute hot air throughout the ro Furnace and fan are never both activated at the same time. The system, initially idle, can be configured for setting the desired temperature within time periods in the form of triplets, i.e. time-fron, tine-to, deaired-temperature. During configuration a user can set as many triplets as they wish, and one triplet may override another with identical data. Upon entering configuration mode, the system will produce a beep sound, and a led light will switch on and stay on as long as the syste s under configuration. Once a user has completed their entries of desired temperature(s), they can indicate the successful completion of configuration, thus letting the system get back to the During configuration, the system allows the user to cancel the current mode in which case the system gets back to the initial idle mode while producing a prolonged beep sound. Triplets that are entered prior to canellation are still registered and considered. Additionally, during configuration a timer is active which, after an inactivity for 1 minute, will cause the system to become idle. Once idle, the system goes into the following cycle which repeats every 2 minutes: It will read the current time and, based on its configuration, it will subsequently determine what is the desired temperature. The system will read the currnt room temperature, and if it is not less than the desired temperature, then it will do nothing, but to repeat the cycle. However if the current temperature is less than one degree lower than the desired temperature, then the system turns the furnace on to build up the desired temperature. During warming up, the furnace remains on, and the system goes into the following cycle which repeats every 3 minutes: It reads in the temperature within the furnace and if it less than a degree higher than the desired temperature, then it will do nothing, but to repeat the cycle. When the furnace temperature reaches a degree higher than the desired temperature, then the system goes back to being idle while turning on the fan in order to blow hot air into the room while at the same time producing a "click" sound. The system allows a user to interrupt warming up in order to perform configuration (as discussed above). The furnace cannot be on during system configuration. When idle, the system can be shut off. When the system is off, both fan and furnace must be switched off