\documentclass[11pt,twoside]{article}\makeatletter

\IfFileExists{xcolor.sty}%
  {\RequirePackage{xcolor}}%
  {\RequirePackage{color}}
\usepackage{colortbl}
\usepackage{wrapfig}
\usepackage{ifxetex}
\ifxetex
  \usepackage{fontspec}
  \usepackage{xunicode}
  \catcode`⃥=\active \def⃥{\textbackslash}
  \catcode`❴=\active \def❴{\{}
  \catcode`❵=\active \def❵{\}}
  \def\textJapanese{\fontspec{Noto Sans CJK JP}}
  \def\textChinese{\fontspec{Noto Sans CJK SC}}
  \def\textKorean{\fontspec{Noto Sans CJK KR}}
  \setmonofont{DejaVu Sans Mono}
  
\else
  \IfFileExists{utf8x.def}%
   {\usepackage[utf8x]{inputenc}
      \PrerenderUnicode{–}
    }%
   {\usepackage[utf8]{inputenc}}
  \usepackage[english]{babel}
  \usepackage[T1]{fontenc}
  \usepackage{float}
  \usepackage[]{ucs}
  \uc@dclc{8421}{default}{\textbackslash }
  \uc@dclc{10100}{default}{\{}
  \uc@dclc{10101}{default}{\}}
  \uc@dclc{8491}{default}{\AA{}}
  \uc@dclc{8239}{default}{\,}
  \uc@dclc{20154}{default}{ }
  \uc@dclc{10148}{default}{>}
  \def\textschwa{\rotatebox{-90}{e}}
  \def\textJapanese{}
  \def\textChinese{}
  \IfFileExists{tipa.sty}{\usepackage{tipa}}{}
\fi
\def\exampleFont{\ttfamily\small}
\DeclareTextSymbol{\textpi}{OML}{25}
\usepackage{relsize}
\RequirePackage{array}
\def\@testpach{\@chclass
 \ifnum \@lastchclass=6 \@ne \@chnum \@ne \else
  \ifnum \@lastchclass=7 5 \else
   \ifnum \@lastchclass=8 \tw@ \else
    \ifnum \@lastchclass=9 \thr@@
   \else \z@
   \ifnum \@lastchclass = 10 \else
   \edef\@nextchar{\expandafter\string\@nextchar}%
   \@chnum
   \if \@nextchar c\z@ \else
    \if \@nextchar l\@ne \else
     \if \@nextchar r\tw@ \else
   \z@ \@chclass
   \if\@nextchar |\@ne \else
    \if \@nextchar !6 \else
     \if \@nextchar @7 \else
      \if \@nextchar (8 \else
       \if \@nextchar )9 \else
  10
  \@chnum
  \if \@nextchar m\thr@@\else
   \if \@nextchar p4 \else
    \if \@nextchar b5 \else
   \z@ \@chclass \z@ \@preamerr \z@ \fi \fi \fi \fi
   \fi \fi  \fi  \fi  \fi  \fi  \fi \fi \fi \fi \fi \fi}
\gdef\arraybackslash{\let\\=\@arraycr}
\def\@textsubscript#1{{\m@th\ensuremath{_{\mbox{\fontsize\sf@size\z@#1}}}}}
\def\Panel#1#2#3#4{\multicolumn{#3}{){\columncolor{#2}}#4}{#1}}
\def\abbr{}
\def\corr{}
\def\expan{}
\def\gap{}
\def\orig{}
\def\reg{}
\def\ref{}
\def\sic{}
\def\persName{}\def\name{}
\def\placeName{}
\def\orgName{}
\def\textcal#1{{\fontspec{Lucida Calligraphy}#1}}
\def\textgothic#1{{\fontspec{Lucida Blackletter}#1}}
\def\textlarge#1{{\large #1}}
\def\textoverbar#1{\ensuremath{\overline{#1}}}
\def\textquoted#1{‘#1’}
\def\textsmall#1{{\small #1}}
\def\textsubscript#1{\@textsubscript{\selectfont#1}}
\def\textxi{\ensuremath{\xi}}
\def\titlem{\itshape}
\newenvironment{biblfree}{}{\ifvmode\par\fi }
\newenvironment{bibl}{}{}
\newenvironment{byline}{\vskip6pt\itshape\fontsize{16pt}{18pt}\selectfont}{\par }
\newenvironment{citbibl}{}{\ifvmode\par\fi }
\newenvironment{docAuthor}{\ifvmode\vskip4pt\fontsize{16pt}{18pt}\selectfont\fi\itshape}{\ifvmode\par\fi }
\newenvironment{docDate}{}{\ifvmode\par\fi }
\newenvironment{docImprint}{\vskip 6pt}{\ifvmode\par\fi }
\newenvironment{docTitle}{\vskip6pt\bfseries\fontsize{22pt}{25pt}\selectfont}{\par }
\newenvironment{msHead}{\vskip 6pt}{\par}
\newenvironment{msItem}{\vskip 6pt}{\par}
\newenvironment{rubric}{}{}
\newenvironment{titlePart}{}{\par }

\newcolumntype{L}[1]{){\raggedright\arraybackslash}p{#1}}
\newcolumntype{C}[1]{){\centering\arraybackslash}p{#1}}
\newcolumntype{R}[1]{){\raggedleft\arraybackslash}p{#1}}
\newcolumntype{P}[1]{){\arraybackslash}p{#1}}
\newcolumntype{B}[1]{){\arraybackslash}b{#1}}
\newcolumntype{M}[1]{){\arraybackslash}m{#1}}
\definecolor{label}{gray}{0.75}
\def\unusedattribute#1{\sout{\textcolor{label}{#1}}}
\DeclareRobustCommand*{\xref}{\hyper@normalise\xref@}
\def\xref@#1#2{\hyper@linkurl{#2}{#1}}
\begingroup
\catcode`\_=\active
\gdef_#1{\ensuremath{\sb{\mathrm{#1}}}}
\endgroup
\mathcode`\_=\string"8000
\catcode`\_=12\relax

\usepackage[a4paper,twoside,lmargin=1in,rmargin=1in,tmargin=1in,bmargin=1in,marginparwidth=0.75in]{geometry}
\usepackage{framed}

\definecolor{shadecolor}{gray}{0.95}
\usepackage{longtable}
\usepackage[normalem]{ulem}
\usepackage{fancyvrb}
\usepackage{fancyhdr}
\usepackage{graphicx}
\usepackage{marginnote}

\renewcommand{\@cite}[1]{#1}


\renewcommand*{\marginfont}{\itshape\footnotesize}

\def\Gin@extensions{.pdf,.png,.jpg,.mps,.tif}

  \pagestyle{fancy}

\usepackage[pdftitle={Model-Based Analysis of Safety Critical Validation Algorithm},
 pdfauthor={}]{hyperref}
\hyperbaseurl{}

	 \paperwidth210mm
	 \paperheight297mm
              
\def\@pnumwidth{1.55em}
\def\@tocrmarg {2.55em}
\def\@dotsep{4.5}
\setcounter{tocdepth}{3}
\clubpenalty=8000
\emergencystretch 3em
\hbadness=4000
\hyphenpenalty=400
\pretolerance=750
\tolerance=2000
\vbadness=4000
\widowpenalty=10000

\renewcommand\section{\@startsection {section}{1}{\z@}%
     {-1.75ex \@plus -0.5ex \@minus -.2ex}%
     {0.5ex \@plus .2ex}%
     {\reset@font\Large\bfseries}}
\renewcommand\subsection{\@startsection{subsection}{2}{\z@}%
     {-1.75ex\@plus -0.5ex \@minus- .2ex}%
     {0.5ex \@plus .2ex}%
     {\reset@font\Large}}
\renewcommand\subsubsection{\@startsection{subsubsection}{3}{\z@}%
     {-1.5ex\@plus -0.35ex \@minus -.2ex}%
     {0.5ex \@plus .2ex}%
     {\reset@font\large}}
\renewcommand\paragraph{\@startsection{paragraph}{4}{\z@}%
     {-1ex \@plus-0.35ex \@minus -0.2ex}%
     {0.5ex \@plus .2ex}%
     {\reset@font\normalsize}}
\renewcommand\subparagraph{\@startsection{subparagraph}{5}{\parindent}%
     {1.5ex \@plus1ex \@minus .2ex}%
     {-1em}%
     {\reset@font\normalsize\bfseries}}


\def\l@section#1#2{\addpenalty{\@secpenalty} \addvspace{1.0em plus 1pt}
 \@tempdima 1.5em \begingroup
 \parindent \z@ \rightskip \@pnumwidth 
 \parfillskip -\@pnumwidth 
 \bfseries \leavevmode #1\hfil \hbox to\@pnumwidth{\hss #2}\par
 \endgroup}
\def\l@subsection{\@dottedtocline{2}{1.5em}{2.3em}}
\def\l@subsubsection{\@dottedtocline{3}{3.8em}{3.2em}}
\def\l@paragraph{\@dottedtocline{4}{7.0em}{4.1em}}
\def\l@subparagraph{\@dottedtocline{5}{10em}{5em}}
\@ifundefined{c@section}{\newcounter{section}}{}
\@ifundefined{c@chapter}{\newcounter{chapter}}{}
\newif\if@mainmatter 
\@mainmattertrue
\def\chaptername{Chapter}
\def\frontmatter{%
  \pagenumbering{roman}
  \def\thechapter{\@roman\c@chapter}
  \def\theHchapter{\roman{chapter}}
  \def\thesection{\@roman\c@section}
  \def\theHsection{\roman{section}}
  \def\@chapapp{}%
}
\def\mainmatter{%
  \cleardoublepage
  \def\thechapter{\@arabic\c@chapter}
  \setcounter{chapter}{0}
  \setcounter{section}{0}
  \pagenumbering{arabic}
  \setcounter{secnumdepth}{6}
  \def\@chapapp{\chaptername}%
  \def\theHchapter{\arabic{chapter}}
  \def\thesection{\@arabic\c@section}
  \def\theHsection{\arabic{section}}
}
\def\backmatter{%
  \cleardoublepage
  \setcounter{chapter}{0}
  \setcounter{section}{0}
  \setcounter{secnumdepth}{2}
  \def\@chapapp{\appendixname}%
  \def\thechapter{\@Alph\c@chapter}
  \def\theHchapter{\Alph{chapter}}
  \appendix
}
\newenvironment{bibitemlist}[1]{%
   \list{\@biblabel{\@arabic\c@enumiv}}%
       {\settowidth\labelwidth{\@biblabel{#1}}%
        \leftmargin\labelwidth
        \advance\leftmargin\labelsep
        \@openbib@code
        \usecounter{enumiv}%
        \let\p@enumiv\@empty
        \renewcommand\theenumiv{\@arabic\c@enumiv}%
	}%
  \sloppy
  \clubpenalty4000
  \@clubpenalty \clubpenalty
  \widowpenalty4000%
  \sfcode`\.\@m}%
  {\def\@noitemerr
    {\@latex@warning{Empty `bibitemlist' environment}}%
    \endlist}

\def\tableofcontents{\section*{\contentsname}\@starttoc{toc}}
\parskip0pt
\parindent1em
\def\Panel#1#2#3#4{\multicolumn{#3}{){\columncolor{#2}}#4}{#1}}
\newenvironment{reflist}{%
  \begin{raggedright}\begin{list}{}
  {%
   \setlength{\topsep}{0pt}%
   \setlength{\rightmargin}{0.25in}%
   \setlength{\itemsep}{0pt}%
   \setlength{\itemindent}{0pt}%
   \setlength{\parskip}{0pt}%
   \setlength{\parsep}{2pt}%
   \def\makelabel##1{\itshape ##1}}%
  }
  {\end{list}\end{raggedright}}
\newenvironment{sansreflist}{%
  \begin{raggedright}\begin{list}{}
  {%
   \setlength{\topsep}{0pt}%
   \setlength{\rightmargin}{0.25in}%
   \setlength{\itemindent}{0pt}%
   \setlength{\parskip}{0pt}%
   \setlength{\itemsep}{0pt}%
   \setlength{\parsep}{2pt}%
   \def\makelabel##1{\upshape ##1}}%
  }
  {\end{list}\end{raggedright}}
\newenvironment{specHead}[2]%
 {\vspace{20pt}\hrule\vspace{10pt}%
  \phantomsection\label{#1}\markright{#2}%

  \pdfbookmark[2]{#2}{#1}%
  \hspace{-0.75in}{\bfseries\fontsize{16pt}{18pt}\selectfont#2}%
  }{}
      \def\TheFullDate{2017 2017-01-15 (revised: 12 Year 2017 15 January 2017)}
\def\TheID{\makeatother }
\def\TheDate{2017 2017-01-15}
\title{Model-Based Analysis of Safety Critical Validation Algorithm}
\author{}\makeatletter 
\makeatletter
\newcommand*{\cleartoleftpage}{%
  \clearpage
    \if@twoside
    \ifodd\c@page
      \hbox{}\newpage
      \if@twocolumn
        \hbox{}\newpage
      \fi
    \fi
  \fi
}
\makeatother
\makeatletter
\thispagestyle{empty}
\markright{\@title}\markboth{\@title}{\@author}
\renewcommand\small{\@setfontsize\small{9pt}{11pt}\abovedisplayskip 8.5\p@ plus3\p@ minus4\p@
\belowdisplayskip \abovedisplayskip
\abovedisplayshortskip \z@ plus2\p@
\belowdisplayshortskip 4\p@ plus2\p@ minus2\p@
\def\@listi{\leftmargin\leftmargini
               \topsep 2\p@ plus1\p@ minus1\p@
               \parsep 2\p@ plus\p@ minus\p@
               \itemsep 1pt}
}
\makeatother
\fvset{frame=single,numberblanklines=false,xleftmargin=5mm,xrightmargin=5mm}
\fancyhf{} 
\setlength{\headheight}{14pt}
\fancyhead[LE]{\bfseries\leftmark} 
\fancyhead[RO]{\bfseries\rightmark} 
\fancyfoot[RO]{}
\fancyfoot[CO]{\thepage}
\fancyfoot[LO]{\TheID}
\fancyfoot[LE]{}
\fancyfoot[CE]{\thepage}
\fancyfoot[RE]{\TheID}
\hypersetup{citebordercolor=0.75 0.75 0.75,linkbordercolor=0.75 0.75 0.75,urlbordercolor=0.75 0.75 0.75,bookmarksnumbered=true}
\fancypagestyle{plain}{\fancyhead{}\renewcommand{\headrulewidth}{0pt}}

\date{}
\usepackage{authblk}

\providecommand{\keywords}[1]
{
\footnotesize
  \textbf{\textit{Index terms---}} #1
}

\usepackage{graphicx,xcolor}
\definecolor{GJBlue}{HTML}{273B81}
\definecolor{GJLightBlue}{HTML}{0A9DD9}
\definecolor{GJMediumGrey}{HTML}{6D6E70}
\definecolor{GJLightGrey}{HTML}{929497} 

\renewenvironment{abstract}{%
   \setlength{\parindent}{0pt}\raggedright
   \textcolor{GJMediumGrey}{\rule{\textwidth}{2pt}}
   \vskip16pt
   \textcolor{GJBlue}{\large\bfseries\abstractname\space}
}{%   
   \vskip8pt
   \textcolor{GJMediumGrey}{\rule{\textwidth}{2pt}}
   \vskip16pt
}

\usepackage[absolute,overlay]{textpos}

\makeatother 
      \usepackage{lineno}
      \linenumbers
      
\begin{document}

             \author[1]{Kushal K  S}

             \author[2]{Dr. Manju  Nanda}

             \author[3]{J  Jayanthi}

             \affil[1]{  CSIR National Aerospace Laboratories}

\renewcommand\Authands{ and }

\date{\small \em Received: 15 December 2016 Accepted: 31 December 2016 Published: 15 January 2017}

\maketitle


\begin{abstract}
        


Safe operation of a critical embedded system requires reliable information about the state of the system and signal condition of the system. Validity of sensors which measure the process variables are of great importance. Signal validation comprises of detection, isolation and characterization of faulty signals. Signals that are validated are critical for their increased availability in the system. Model-Based Engineering (MBE) approach provides means of modeling, analyzing, and validating the signals for critical embedded system design, and development. The abstract nature of the models provides mechanisms to analyze verify and validate the system functionality, at a much early stage in their development process. In this paper we present MBE approach to analyze the input signal processing algorithm with the case study of analog signal for Stall Warning System (SWS) of an aircraft using NI LabVIEW. The approach helps in analysing the functionality and completeness of the algorithm, mathematically and by simulation. The validation of analog signals with different frequencies and amplitude establishes data prudency and maintains the integrity of avionics systems. The result of this approach highlights the advantage of using MBE which enables in analysing the data algorithm for its correctness and guarantees the properties of the model early in the development life-cycle. MBE approach also helps in re-assuring the integrity of the system, before it is developed. This also terminates the contiguous data set and annunciates the sensor fault conditions

\end{abstract}


\keywords{analog input processing, stall warning system (SWS), model-based engineering (MBE), safety- critical system, NI LABVIEW.}

\begin{textblock*}{18cm}(1cm,1cm) % {block width} (coords) 
\textcolor{GJBlue}{\LARGE Global Journals \LaTeX\ JournalKaleidoscope\texttrademark}
\end{textblock*}

\begin{textblock*}{18cm}(1.4cm,1.5cm) % {block width} (coords) 
\textcolor{GJBlue}{\footnotesize \\ Artificial Intelligence formulated this projection for compatibility purposes from the original article published at Global Journals. However, this technology is currently in beta. \emph{Therefore, kindly ignore odd layouts, missed formulae, text, tables, or figures.}}
\end{textblock*}


\let\tabcellsep& 	 	 		 
\section[{Introduction}]{Introduction}\par
alidity of the data input-output of Safety-Critical Systems such as avionics systems, medical instruments, and nuclear systems is critical and needs to be analyzed for its functionality, performance, and safety. Complex avionics systems encompassing multiple critical sensor data associated with the plurality of sensors that needs to be validated for the correct data and also detect fault condition of the sensor. Productivity challenges are on the rise with the increase in the complexity of the software involved in Safety-Critical Systems. Such systems are considered to be least intolerant with safety of the overall functionality of the system, as well as dependency and reliability of the system. Model-Based Engineering (MBE) approaches provide the means of creating and analyzing the models of the Safety-Critical System. These approaches accomplish the task of providing prediction and analyses capabilities of various operational qualitative attributes like performance, productivity, reliability and security. In the development life-cycle, with the application of Model-Based Engineering (MBE) approaches, the system-level problems, are detected at an early stage during their development process which are usually discovered during the system integration and acceptance test, using the conventional approaches. This avoids in rework during the later stages of their development and also minimizes the maintenance cost. The paradigm of developing the application software for Safety-Critical Systems are shifting with the introduction of Model-Based Engineering approaches. The graphical representation of the Safety-Critical System control algorithm application software, using MBE, serves the primary purpose of representation of the application software as a re-usable executable model. This can be re-used at any stage during their development process in the entire life-cycle. This executable model analyzes the predicted system properties and validates them against the system implementation, considering the evaluation of various quality assurances attributes in the course of analyses.\par
Models representing a Safety-Critical System integument of data-flow, topology and the behavioral aspects of the application software, are created using a suitable modeling language. This modeling language is regarded as formal representation of the application software being developed with precise perception of the actual implementation of the control logic. This ultimately forms the basis for conformance testing against the system requirements.\par
Modeling language used in creating the models serves as a multi-purpose graphical representation encompassing all the aspects of the Safety-Critical System application software as an abstract. Laboratory Virtual Instrument Engineering Workbench (LabVIEW), a system design and development environment from National Instruments, in conjunction with the Visual Programming Language (VPL) \hyperref[b0]{[1]} provides the means of creating the Safety-Critical System models. LabVIEW basically makes use of VPL, wherein the application software is created by manipulating the software components graphically as symbols along with the textual notations. LabVIEW makes use of "G" language -a graphical language used for systems design and simulation.\par
Using LabVIEW the Safety-Critical System application software model is created precisely in coherence with the system requirements, describing all the aspects of the system. This MBE approach with LabVIEW renders the model to define the domain oriented abstractions that define the system components, states, transitions between the states. The validation of such clutter less models to cover different levels of formalities like model checking \hyperref[b2]{[3]}, prototyping and simulation \hyperref[b1]{[2]}. By combining the effectiveness of the domain specific abstract models and its implementations with prototyping and simulation the application software model is validated for its functionality.\par
The paper is organized as follows: section II, provides an insight into the related works carried out with MBE. With section III, we introduce to the characteristic features of analog input signal data in Stall Warning System (SWS) and the need for validation. Afterwards, section IV focuses on the analog input processing algorithm and the implementation of the algorithm for different analog signals of SWS, using LabVIEW. Section V sketch the results and summarize the overall validation process. Section VI concludes the work discussed in the context and comment on future work to be done with this reference. 
\section[{II.}]{II.} 
\section[{Literature Survey}]{Literature Survey}\par
The need to validate the health of the input data signals which are interfaced with certain critical decision making systems is very much essential, in aerospace applications and avionics systems. This helps in the differentiation of the signals as faulty and healthy. The process of differentiating the signals as two different categories, are handled by efficient algorithms developed and implemented. Manju Nanda et al. \hyperref[b3]{[4]} had proposed a contemporary validation algorithm in validating the signals and thus helping the underlying systems in making appropriate critical decisions. Also the need to verify the correctness of the abstracts of the models of a system under test, corresponding to Model-Checking and Model-Based Testing was proposed by Stefan Gulan et.al. \hyperref[b6]{[7]}. The early introduction of these approaches for safety mechanisms relevant to the safety of the software was evaluated with an industrial case study sufficiently to address the relevant failures in the systems and its software components.\par
The exponential growth in the discovery of the system-level faults at the development stage in SDLC process has adverse turn-around effects, such as increase in the cost of development and the rigorous changes that may be subjected to the system and its underlying software components. This can be overcome with the use of Model-Based Analysis and Validation approaches as suggested by Peter H Feiler \hyperref[b7]{[8]}. With MBE a single source approach is provided to the developer to analyze the system for its operational attributes as well as the system qualitative attributes. This is more reliable through model annotations. Also Bringmann et.al. \hyperref[b8]{[9]} has proposed with the help of an industrial case study that the quality assurance with the model-based developments with the introduction of graphically testable models representing the software components of the system under test enables the user to understand the architecture of the algorithm of the software. It was also suggested that it helps in expressing complex, fully automated closed-loop test scenarios in real-time. Using MBE approaches for modeling the software component of a system, it is like performing the actual implementation of the algorithm or the software component and defining their relationship between each other. This was proposed by Andree Blotz et.al \hyperref[b9]{[10]}. The models are created using different languages and are regarded as the formal representation of their functionalities. With all these findings the complex processing algorithm of SWS/AIC i.e. the Analog Input Processing algorithm is modeled using NI LabVIEW. Its operations, capabilities in validating the input data from various aircraft interfaced sensors are discussed in this paper. 
\section[{III.}]{III.} 
\section[{Analog Input Signal Data of SW}]{Analog Input Signal Data of SW}\par
The digital computer based Stall Warning System (SWS)/ Aircraft Interface Computer (AIC) \hyperref[b4]{[5]}, a state-of-art designed around a customized APM2000 module by SAGEM. The module consists of two processing units Motorola MC68060 along with the coprocessor units MC68360, designed as per DO-178B standards \hyperref[b5]{[6]}. The system consists of input interfaces to different signals of types ARINC429, Discrete and Analogous and processes them accordingly. The SWS systems also provide a stall warning by activating the shaker actuator of the aircraft and indicating them suitably through LED, on the Caution Warning Panel (CWP).\par
The analog signals read by APM2000 kernel when invoked by the application software and the inputs that are acquired are converted into digital signals for processing by the processor units using a 12-bit Analog-Digital Converter (ADC). The acquired values are made available to the Analog Input Processing algorithm application software in a specified memory location for further processing by the kernel. Any fault or error during the acquisition is examined and returned after the validation by the Analog Input Processing algorithm application software. 
\section[{a) Angle of Attack (AOA) Sensors Interface}]{a) Angle of Attack (AOA) Sensors Interface}\par
The Angle-Of-Attack (AOA) is the physical angle measured between the chord of the aircraft wing and  
\section[{S}]{S}\par
the relative wind direction. There are basically two AOA vane sensors that act as potentiometers. Both the left and right potentiometer sensors are excited by 11.3V DC power supply. As an analog input for the system, the physical range is from -10° to +40°. The DC analog signal ranges from 0V corresponding to -10°, while 11.3V corresponds to +40°. The value of the sensor reading is stored in the memory and used to estimate the AOA value during validation. 
\section[{b) Fuel Remianing Input Interface}]{b) Fuel Remianing Input Interface}\par
The SWS/AIC have the interface to the fuel system to get the fuel remaining in the fuel tank of the aircraft. This input from the interface is obtained as an analog input from the fuel tank capacitor probes provided for both the left and right channels in the aircraft. The physical analog range of the fuel remaining varies from 0V DC corresponding to 0kg, to 5V DC corresponding to 1000kg. But there is a constraint of minimum fuel remaining to be 12.5kg. The fuel value corresponding to the amount of fuel present during the take-off is stored in the memory location. This value is used for the weight estimation during the validation. 
\section[{c) Torque Pressure Transducer Sensor Input Interface}]{c) Torque Pressure Transducer Sensor Input Interface}\par
The torque pressure transmitter is connected to the torque meter in the cockpit. The SWS/AIC system shall have an interface with the torque pressure transducer and reads the engine torque as an analog input. The transducers are present on both left and right channels of the aircraft. The engine torque input ranges from 0 to 5V DC, corresponding to 0 to 44.34psig equal to 3.684V. Here the torque value being greater than or equal to 16.85psig (38\% or 1.3999V) indicates that the aircraft is ready for take-off.\par
For the landing condition the torque value shall be less than or equal to 20\% (8.868psig or 0.736V) on both the left and right engines. Even if there happens to be a value of 50\% torque on one engine (22.17psig or 1.824V) if the other engine is in-operative with a torque value less than 10\% (4.434psig or 0.368V). 
\section[{d) Pitch Trim Position Sensor Input Interface}]{d) Pitch Trim Position Sensor Input Interface}\par
The SWS/AIC have the interface with the pitch trim potentiometer to get the position of the pitch trim tab as an analog signal from the potentiometer. The pitch trim position sensors are physically combined as a single channel from both the right and left channels. The pitch trim sensor is excited with a voltage value of 11.3V. The analog input signal acquired from the pitch trim position sensor varies from -15o to +8o. This input is used to limit the electrical travel of the actuator. An input voltage value of 11.08V is read when the excitation voltage of 11.3V is provided across the potentiometer with a bias of 5.54V. The error tolerance is defined to be +/-0.065V. 
\section[{e) Hydraulic Pressure Sensor Input Interface}]{e) Hydraulic Pressure Sensor Input Interface}\par
The SWS AIC have been interfaced with the hydraulic pressure sensors to get the value of the hydraulic pressure as analog input. The input range varies from 0-4000psi, corresponding to 0.25V to 5.25V DC.\par
IV. 
\section[{Implementation of Analog Input Processing Algorithm}]{Implementation of Analog Input Processing Algorithm}\par
The continuously time varying signals from a plurality of aircraft interfaces like AOA sensors, Fuel Tank sensors, Pitch Trim sensors, Hydraulic Pressure sensors are obtained and are independent of each other. These signals obtained from various sensors, which are either simplex (from a single source) or duplex (from dual sources) needs to be validated and compared to measure the quality of the signal/data received and indicate it via a validity flag.\par
The rate of change of the signal from the physical system is matched to a sampling rate of 25millisecond. This is the same time duration for which the algorithm is designed to read the signal/data recorded by the sensor. During the continuous acquisition of signal/data from the sensor, for a persistence time of 250millisecond, implying that 3 samples are considered in an averaging window, the rate at which the acquired signal/data changes is constantly monitored. This rate of change is compared with a pre-defined threshold value. The recently acquired signals are compared with the previous samples of signal/data and monitored for their values, which may be well within the specified tolerance value. Based on the comparator output the signal/data is termed as healthy or unhealthy, by monitoring it over the period of persistence time. The process of analyzing the analog input signals is as shown below in Figure \hyperref[fig_1]{1}. The basis for this algorithm is that, any signal acquired from any of the aircraft sensors is to be declared as valid or invalid, based on the fixed sample approach. The acquired signal is declared valid or invalid, over a persistence time of 250ms, based on the comparison with their difference between the current valued signal/data that has been acquired with the previously acquired signal (if nothing then to be considered as zero), termed as Difference |B| and the difference between the last previous valued signal/data to that of the previously acquired signal/data as Difference |A|. The magnitudes of both the differences are then compared with the priori specified tolerance band (default +/-2\% of the nominal value -full range value). This range check is carried out for all the acquired input signals/data and the engineering value conversion is done for the analog inputs. In case the acquired analog input signal is out of bounds of the specified tolerance band, then the output value is clamped to the minimum value if the acquired signal value is less than the minimum value. It is clamped to maximum, if the acquired signal value is more than maximum range specified. This is done along with the storage of the association of the suitable flag status, set either as Valid or Invalid. The purpose of the acquired signal is only for the validity or the invalidity check. For all the analog inputs that are acquired from the sensors, if the signal/data is invalid then the invalid flag is set to TRUE and the output data is latched to a particular valid data that was acquired currently, previously or past the previous acquisition. In case of valid signal/data, the valid flag is set TRUE and the average value of the current, previous and the value past the previously acquired signal/data is latched as the output data. This analog input processing algorithm was developed using Model-Based Engineering (MBE) approach, using LabVIEW from National Instruments. This approach helps in defining the processing control algorithm software components as models that can be re-used and provides more efficiency and robustness as compared with other conventional approaches. 
\section[{Global Journal of Researches in Engineering ( ) Volume XVII Issue I Version I}]{Global Journal of Researches in Engineering ( ) Volume XVII Issue I Version I} 
\section[{1) Functional Translation}]{1) Functional Translation}\par
The LabVIEW tool suite is used in modeling the analog input processing algorithm application software. The models that are designed in the LabVIEW development environment will be termed as Virtual Instruments (VI), as the models virtual represents the physical implementations of the system being designed and developed. This tool suite provides the option of categorically and hierarchically modeling features   The actual system implementation for Hydraulic Pressure Sensor Input Interface is designed as shown in Figure \hyperref[fig_5]{4}. In case of the Hydraulic Pressure Sensor input being invalid the output data is computed based on the lower and upper limits as explained in III.E, and latched to the previous/current/last previous valid data. The valid flag is set to FALSE and there is no computation warning being generated for the Hydraulic Pressure by the SWS/AIC. The block diagram implemented is as per the specifications for its analog input signal/data scaled to its equivalent digital voltage valued array. The range is also validated for Hydraulic Pressure Sensor Input as shown in Figure \hyperref[fig_5]{4}. The array is fed as input into the error injection loop, as shown in Figure \hyperref[fig_6]{5}. This loop is present in all the analog input interface modules. This loop allows the user to define the error value i.e. the user has the liberty to set any error value. The tolerance is to be adjusted to the full scale range of the analog input interface and the array is resized to the actual input array size in this loop.\par
Here in this loop, the privilege of inserting the error value into a particular index of the array is also provided. The error injection is controlled using the LabVIEW control switch termed as Error ON/OFF. This helps in inserting the error value in the index of the array during the simulation, dynamically. This is simulated and as well being considered for computation of the warning suitably from the index/time of its insertion into the array. An error valued data is inserted for a time factor of 25ms, every time in the array. This array of input with or without the error is fed into the Analog Validation and Data Sorting loop for the data to be sorted and validated as per the specified limits.  
\section[{b) Fuel Remaining Input Interface}]{b) Fuel Remaining Input Interface}\par
The Fuel Remaining Input Interface system implementation is done as shown in Figure \hyperref[fig_8]{6}. There are two fuel tanks present in an aircraft. One in the right wing, which corresponds to the right channel while the other in the left wing corresponding to the left channel. During the Analog Validation, in case the right fuel tank input on the right channel is invalid then the output data is computed and latched to the previous/current/last previous valid data. This means that the Analog Input Processing algorithm shall use the average value of the last correct/valid weight estimate and the aircraft with no fuel remaining.\par
The same case applies with the left fuel tank input on the left channel being invalid, the output data is computed and latched to the previous/current/last previous valid data. And the SWS/AIC Analog Input Processing algorithm uses the average value of the last correct/valid weight estimate and the aircraft with no fuel remaining from the left channel. In both these cases, the valid flag is set to FALSE. If the data from either or both the channels are valid then the average value of all the three data sets, i.e. previous valued, current valued and the last previous valued data from the array is computed and the output data is set to the average value. The valid flag is set to TRUE. The process of error injection is repeated for this Sub VI also and the array data corresponding to Fuel Remaining is also sorted and validated using the Analog Input Processing and Data Sorting Sub VI loop, as shown in Figure \hyperref[fig_6]{5}. 
\section[{Fuel Remaining Input Interface Block Diagram as Sub VI c) Angle-Of-Attack Sensors Interface}]{Fuel Remaining Input Interface Block Diagram as Sub VI c) Angle-Of-Attack Sensors Interface}\par
The model implementation with the given specifications in III.A, for Angle-Of-Attack Sensor Interface is as shown below in Figure \hyperref[fig_7]{7}. There are two channels, (Left \& Right Wings) with AOA sensors. The range of the value sensed by the AOA sensor is being validated and the array of inputs is built. The input array is fed into the Analog Input Processing and Data Sorting algorithm Sub VI loop for validation and data sorting, respectively.\par
In case, the left AOA sensor sensed data is invalid then the AOA value shall be computed for the output data and latched to the previous/current/last previous valid data. Similarly in case of the right AOA sensor sensing an invalid data set, then the AOA value shall be computed for the output data and latched to the previous/current/last previous valid data. In both the cases the valid flag is set to FALSE. For the AOA sensors, as is special case, the mounting error for the left channel AOA with respect to the right channel AOA sensor with a zero bias value of 2.3634V is used in the application software, shown in Figure \hyperref[fig_7]{7}, during the data set being valid. Also the dead band of 0.724V and 0.364V shall be used for left AOA and right AOA engineering value conversions. Different fixed error value considerations are being made to distinguish and compute left channel AOA with the right channel AOA, as 1.389o and 0o respectively. A suitable method such as Ratiometric method is used to compute the AOA values for better accuracy.  In case the pitch trim position input is invalid then the data set is computed for the output data and latched to the previous/current/last previous valid data. The valid flag is set to FALSE and a suitable warning shall be generated for the same. In this case of pitch trim sensor invalid data, the pilot switched over to the manual mode from the automated mode. In case if the data is valid, then the valid flag is set to TRUE and the output data is computed based on the average of current, previous and last previous valued data from the array, and latched to it. In case of left engine torque as sensed by the Torque Pressure Transducer sensor, is invalid, and then the output data is computed by the Analog Input Processing algorithm and is latched to the previous/current/last previous valid data. Similarly, in case of right engine torque sensed by the right channel as invalid, the output data is computed and is latched to the previous/current/last previous valid data. In both the cases the valid flag is set to FALSE, and the right/left engine torque is not considered for the takeoff warning computations by SWS/AIC. In case if the data is valid, then the valid flag is set to TRUE and the output data is computed based on the average of current, previous and last previous valued data from the array, and latched to it.  
\section[{Simulation and Analytical Results}]{Simulation and Analytical Results}\par
The actual implementation of the Analog Input Processing application software is modeled using NI LabVIEW. The input data, is as per the values as given below in Table  The inputs are being input to the Analog Input Processing application software algorithm with the help of their respective sensor interface Sub VIs. The input data is up to a maximum of 100 index values and the constant valid data is being fed into the sub-systems. A suitable error vale (in terms of \%), computed on the full scale input range is inserted at suitable index in the input array. Their equivalent DC voltage values are recorded as array values/elements and this is done dynamically, i.e. during the simulation. The system is being simulated for a particular Hydraulic Pressure value as shown in Figure \hyperref[fig_11]{10} or Fuel Remaining as shown in Figure \hyperref[fig_12]{11or} AOA as shown in Figure \hyperref[fig_13]{12} or Pitch Trim position as shown in Figure 13 or Engine Torque as shown in Figure 14. The Error On/Off control, regulates the control of insertion of error value to the specified hydraulic pressure/pitch trim position/fuel remaining/AOA/engine torque pressure value. Here in order to justify the analog input processing algorithm functionality for hydraulic pressure sensor inputs, the hydraulic pressure of 3500psi is considered (within the specified range as given in Table \hyperref[tab_1]{1}). An error value of +/-2\% of 3500psi (\textasciitilde = 4.625V DC) is considered, at suitable time intervals (as shown in the simulation window of Input(HP)). An input array values with 100 elements is recorded as the input array, which is fed into the Analog Input Processing application software algorithm and Data Sorting algorithm loops to validate the data and sort the data as Current Valued,  \hyperref[fig_11]{10}. Similarly for Fuel Remaining the data input of 60kg of fuel is considered. An error value of +/-2\% of 60 kg (\textasciitilde = 0.3V DC) is inserted suitably in the input array of 100 elements at certain time intervals, for 25ms as each sample. The process is repeated as specified in the above section for Hydraulic Pressure Sensor Input Interface. Here it can be observed that the AnalogValidFlagList is set to TRUE as there is a valid data and the Invalid Sample Window count is 0.  A maximum input value of 8deg is considered as input for the Pitch Trim Position sensor input interface. An error value of +/-2\% of the maximum full range scale (\textasciitilde = 8.00002V DC) is considered and inserted into the array of 100 input elements, for further processing and sorting. During the simulation, as can be seen in Figure 13, at the index value of 40, there exists an invalidity of the samples. This is being analyzed and the AnalogValidFlagList is set to FALSE. The Invalid Sample Window count is set to 1, as there exists an invalidity, which can be inferred from the magnitude of the difference values (i.e. 0.320002) in this case at that time period is way above the priori specified tolerance value. The RawAnalogValidList corresponding to the output data is set to 0 and will be replaced with the valid Current/Previous./Last Previous value from the sorted input array upon the completion of the validation process by the Analog Input Processing application software algorithm  mathematically that proves the correctness and effectiveness of the algorithm and the need for such an approach. The objective of achieving a high reliable processing algorithm, with more complexity was successfully met.\par
In this paper we have proposed and implemented a novel MBE approach with the help of NI LabVIEW tool suite, with the Analog Input Processing software algorithm as a case study. The results obtained from the analyses of these models were reliable, versatile and also suitably substantiated in the removal of vexation. Validation of the implementation against the system specified requirements and the analysis of the output data against the test cases obtained during the conventional test approaches were compared and no deviations were observed. This also helped in addressing the unrealistic and unreliable situations early during the development phase, thereby reducing the overall work around cost in fixing the bug/error. VII.\begin{figure}[htbp]
\noindent\textbf{}\includegraphics[]{image-2.png}
\caption{\label{fig_0}}\end{figure}
 \begin{figure}[htbp]
\noindent\textbf{1}\includegraphics[]{image-3.png}
\caption{\label{fig_1}Figure 1 :}\end{figure}
 \begin{figure}[htbp]
\noindent\textbf{}\includegraphics[]{image-4.png}
\caption{\label{fig_2}}\end{figure}
 \begin{figure}[htbp]
\noindent\textbf{2}\includegraphics[]{image-5.png}
\caption{\label{fig_3}Figure 2 :}\end{figure}
 \begin{figure}[htbp]
\noindent\textbf{3}\includegraphics[]{image-6.png}
\caption{\label{fig_4}Figure 3 :}\end{figure}
 \begin{figure}[htbp]
\noindent\textbf{4}\includegraphics[]{image-7.png}
\caption{\label{fig_5}Figure 4 :}\end{figure}
 \begin{figure}[htbp]
\noindent\textbf{5}\includegraphics[]{image-8.png}
\caption{\label{fig_6}Figure 5 :}\end{figure}
 \begin{figure}[htbp]
\noindent\textbf{7}\includegraphics[]{image-9.png}
\caption{\label{fig_7}Figure 7 :}\end{figure}
 \begin{figure}[htbp]
\noindent\textbf{6}\includegraphics[]{image-10.png}
\caption{\label{fig_8}Figure 6 :}\end{figure}
 \begin{figure}[htbp]
\noindent\textbf{8}\includegraphics[]{image-11.png}
\caption{\label{fig_9}Figure 8 :}\end{figure}
 \begin{figure}[htbp]
\noindent\textbf{9}\includegraphics[]{image-12.png}
\caption{\label{fig_10}Figure 9 :}\end{figure}
 \begin{figure}[htbp]
\noindent\textbf{10}\includegraphics[]{image-13.png}
\caption{\label{fig_11}Figure 10 :}\end{figure}
 \begin{figure}[htbp]
\noindent\textbf{11}\includegraphics[]{image-14.png}
\caption{\label{fig_12}Figure 11 :}\end{figure}
 \begin{figure}[htbp]
\noindent\textbf{12}\includegraphics[]{image-15.png}
\caption{\label{fig_13}Figure 12 :}\end{figure}
    \begin{figure}[htbp]
\noindent\textbf{1} \par 
\begin{longtable}{}
\end{longtable} \par
 
\caption{\label{tab_1}Table 1 :}\end{figure}
 \begin{figure}[htbp]
\noindent\textbf{} \par 
\begin{longtable}{P{0.030808550185873605\textwidth}P{0.18090148698884756\textwidth}P{0.16668215613382897\textwidth}P{0.12323420074349442\textwidth}P{0.18011152416356876\textwidth}P{0.036338289962825274\textwidth}P{0.04976765799256506\textwidth}P{0.0229089219330855\textwidth}P{0.059247211895910784\textwidth}}
Sl No\tabcellsep Signal Name\tabcellsep Physical Range\tabcellsep Scale Factor\tabcellsep Bias\tabcellsep \multicolumn{2}{l}{Accuracy Resolution}\tabcellsep Refresh Rate\\
1.\tabcellsep RawAOALA\tabcellsep \multicolumn{2}{l}{-10 to +40°4.8216 deg/V}\tabcellsep \multicolumn{4}{l}{2.074V ±0.0152 V 0.0224 deg once/ 25 ms cycle}\\
2.\tabcellsep RawAOALB*\tabcellsep -10 to +40\tabcellsep 4.8216 deg/V\tabcellsep \multicolumn{4}{l}{2.074V ±0.0152 V 0.0224 deg once/ 25 ms cycle}\\
3.\tabcellsep RawAOARA\tabcellsep \textunderscore 10 to +40\tabcellsep \multicolumn{5}{l}{4.8721 deg/V 2.0525V ±0.0152 V 0.0224 deg once/ 25 ms cycle}\\
\multicolumn{2}{l}{4. RawAOA RB*}\tabcellsep -10 to +40\tabcellsep \multicolumn{5}{l}{4.8721 deg/V 2.0525V ±0.0152 V 0.0224 deg once/ 25 ms cycle}\\
5.\tabcellsep Fuel Remaining left (LftFuelTank)\tabcellsep 0-1000 kg for\tabcellsep 200kg/V\tabcellsep -\tabcellsep ±0.0152 V\tabcellsep 1.016 kg\tabcellsep once/ 25 ms cycle\\
6.\tabcellsep Fuel Remaining right(RgtFuelTank)\tabcellsep 0-1000 kg for\tabcellsep 200kg/V\tabcellsep -\tabcellsep ±0.0152 V\tabcellsep \multicolumn{2}{l}{1.016 kg once / 25 ms cycle}\\
7.\tabcellsep Left Engine Torque (EngTorqueL)\tabcellsep \multicolumn{2}{l}{0 -44.34psig 12.035 psig/V}\tabcellsep -\tabcellsep ±0.0152 V\tabcellsep \multicolumn{2}{l}{0.061 psig once / 25ms cycle}\\
8. 9. 10.\tabcellsep Right Engine Torque (EngTorqueR) Pitch trim position (PtchTrimPos) Hydraulic pressure (HydPress)\tabcellsep \multicolumn{2}{l}{0 -44.34psig 12.035 psig/V -15 to +8 deg. 5.3097 0 / V 0-4000 PSI 800 PSI / V}\tabcellsep \multicolumn{4}{l}{-5.54V 0.25 V ±0.0152 V 4.05 psi ±0.0152 V 0.061 psig once / 25 ms cycle ±0.0152 V 0.0269 deg once / 25 ms cycle once / 25 ms cycle}\tabcellsep ( ) Volume XVII Issue I Version I\\
\tabcellsep \tabcellsep \tabcellsep \tabcellsep \tabcellsep \tabcellsep \tabcellsep \tabcellsep of Researches in Engineering\\
\tabcellsep \tabcellsep \tabcellsep \tabcellsep \tabcellsep \tabcellsep \tabcellsep \tabcellsep Global Journal\end{longtable} \par
 
\caption{\label{tab_2}}\end{figure}
 			\footnote{Year 2017 D © 2017 Global Journals Inc. (US) Model-Based Analysis of Safety Critical Validation Algorithm} 			\footnote{© 2017 Global Journals Inc. (US)} 			\footnote{D © 2017 Global Journals Inc. (US) Model-Based Analysis of Safety Critical Validation Algorithm} 			\footnote{Year 2017 D Model-Based Analysis of Safety Critical Validation Algorithm} 		 		\backmatter   			 
\subsection[{Acknowledgements}]{Acknowledgements}\par
The authors would like to thank the Director of CSIR-NAL, Bengaluru, for supporting this work. 			  			  				\begin{bibitemlist}{1}
\bibitem[Erbay and Seyfettin ()]{b12}\label{b12} 	 		\textit{A PC-Based Signal Validation System for Nuclear Power Plants},  		 			Ali Erbay 		,  		 			Seyfettin 		.  		 \url{http://trace.ten-nessee.edu/utk\textunderscore gradthes/2583}  		1994.  		 			University of Tennessee 		 	 	 (Master's Thesis) 
\bibitem[Ray and Luck (1991)]{b11}\label{b11} 	 		‘An introduction to sensor signal validation in redundant measurement systems’.  		 			A Ray 		,  		 			R Luck 		.  		 \xref{http://dx.doi.org/10.1109/37.67675}{10.1109/37.67675}.  	 	 		\textit{IEEE Control Systems},  				Feb. 1991. 11 p. .  	 
\bibitem[Jost et al. (2014)]{b0}\label{b0} 	 		‘Graphical programming environments for educational robots: Open roberta-yet another one?’.  		 			B Jost 		,  		 			M Ketterl 		,  		 			R Budde 		,  		 			T Leimbach 		.  	 	 		\textit{IEEE International Symposium on},  				2014. 2014 Dec 10. IEEE. p. .  	 	 (, InMultimedia (ISM)) 
\bibitem[Gulan et al. (2015)]{b6}\label{b6} 	 		‘Model-Based Analysis for Safety Critical Software’.  		 			S Gulan 		,  		 			J Harnisch 		,  		 			S Johr 		,  		 			R Kretschmer 		,  		 			S Rieger 		,  		 			R Zalman 		.  	 	 		\textit{InInternational Conference on Computer Safety, Reliability, and Security},  				2015 Sep 22. Springer International Publishing. p. .  	 
\bibitem[Blotz et al. ()]{b9}\label{b9} 	 		\textit{Model-based software engineering and Ada: Synergy for the development of safety-critical systems},  		 			A Blotz 		,  		 			F Huber 		,  		 			H Lötzbeyer 		,  		 			A Pretschner 		,  		 			O Slotosch 		,  		 			H P Zängerl 		.  		2002. 2002. Ada, Deutschland.  	 
\bibitem[Bringmann and Krämer (2008)]{b8}\label{b8} 	 		‘Model-based testing of automotive systems’.  		 			E Bringmann 		,  		 			A Krämer 		.  	 	 		\textit{In2008 1st International Conference on Software Testing, Verification, and Validation},  				2008 Apr 9. IEEE. p. .  	 
\bibitem[Feiler (2010)]{b7}\label{b7} 	 		\textit{Model-based validation of safety-critical embedded systems. InAerospace Conference},  		 			P H Feiler 		.  		2010 IEEE 2010 Mar 6. IEEE. p. .  	 
\bibitem[Nanda et al. ()]{b3}\label{b3} 	 		‘Novel Validation Algorithms for Safety Critical Embedded Software’.  		 			M Nanda 		,  		 			J Jayanthi 		,  		 			S Rao 		.  		 \xref{http://dx.doi.org/10.1049/cp:20080731}{10.1049/cp:20080731}.  	 	 		\textit{rd IET International Conference on System Safety},  				 (Birmingham)  		2008. 2008. 3 p. .  	 
\bibitem[Yeh ()]{b10}\label{b10} 	 		‘Safety critical avionics for the 777 primary flight controls system’.  		 			Y C Yeh 		.  		 \xref{http://dx.doi.org/10.1109/DASC.2001.96-3311}{10.1109/DASC.2001.96-3311}.  	 	 		\textit{20th DASC. 20th Digital Avionics Systems Conference (Cat. No.01CH37219)},  				 (Daytona Beach, FL)  		2001. 1 p. .  	 
\bibitem[Software Considerations in Airborne Systems and Equipment Certification (2011)]{b5}\label{b5} 	 		\textit{Software Considerations in Airborne Systems and Equipment Certification},  		 \url{http://www.rtca.org/}  		December 2011.  	 	 (RTCA) 
\bibitem[Dr et al. (2015)]{b4}\label{b4} 	 		\textit{Software Requirements Data Document for SARAS SWS/AIC System},  		 			Manju Dr 		,  		 			G K Nanda 		,  		 			K P Singh 		,  		 			Srikanth 		.  		Dec 2015. Bengaluru. p. .  		 			CSIR-National Aerospace Laboratories 		 	 
\bibitem[Philipps and Slotosch ()]{b2}\label{b2} 	 		‘The quest for correct systems: Model checking of diagrams and datatypes’.  		 			J Philipps 		,  		 			O Slotosch 		.  	 	 		\textit{APSEC'99) Proceedings. Sixth Asia Pacific},  				1999. 1999. IEEE. p. .  	 
\bibitem[Huber et al. (1998)]{b1}\label{b1} 	 		\textit{Tool Supported Specification and Simulation of Distributed Systems},  		 			F Huber 		,  		 			S Molterer 		,  		 			A Rausch 		,  		 			B Schätz 		,  		 			M Sihling 		,  		 			O Slotosch 		.  		1998 Apr 20. Inpdse. p. 155.  	 
\end{bibitemlist}
 			 		 	 
\end{document}
