\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={Performance Evaluation of Software using Formal Methods},
 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{2020-01-15 (revised: 15 January 2020)}
\def\TheID{\makeatother }
\def\TheDate{2020-01-15}
\title{Performance Evaluation of Software using Formal Methods}
\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]{Akinsola, Jide E.  T.}

             \author[2]{Kuyoro, Afolashade,  O.}

             \author[3]{Adeagbo, Moruf  A.}

             \author[4]{Awoseyi, Ayomikun  A.}

\renewcommand\Authands{ and }

\date{\small \em Received: 10 December 2019 Accepted: 2 January 2020 Published: 15 January 2020}

\maketitle


\begin{abstract}
        


Formal Methods (FMs) can be used in varied areas of applications and to solve critical and fundamental problems of Performance Evaluation (PE). Modelling and analysis techniques can be used for both system and software performance evaluation. The functional features and performance properties of modern software used for performance evaluation has become so intertwined.Traditional models and methods for performance evaluation has been studied widely which culminated into the modern models and methods for system and software engineering evaluation such as formal methods. Techniques have transcended from functionality to performance modeling and analysis. Formal models help in identifying faulty reasoning far earlier than in traditional design; and formal specification has proved useful even on already existing software and systems. Formal approach eliminates ambiguity. The basic and final goal of the performance evaluation technique is to come to a conclusion, whether the software and system are working in a good condition or satisfactorily.

\end{abstract}


\keywords{formal methods, performance evaluation, performance modeling, software performance evaluation, machine learning, markov chains, queuing networks.}

\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
he term Formal Methods (FM) refers to the use of mathematical modelling, calculation and prediction in the specification, design, analysis and assurance of computer systems and software. The reason it is called formal methods rather than mathematical modelling of software is to highlight the character of the mathematics involved \hyperref[b27]{(Rushby, 1995)}.\par
According to Wikipedia, the use of formal methods for software and hardware design is motivated by the expectation that, as in other engineering disciplines, performing appropriate mathematical analyses can contribute to the reliability and robustness of a design.\par
Formal methods (FM) or Formal Techniques (FT) for performance evaluation include formalisms for performance modeling (Markov chains, queuing networks, stochastic Petri nets, and stochastic process algebras), equivalence checking and model checking, efficient solution techniques, and software performance engineering \hyperref[b7]{(Bernardo \& Hillston, 2007)}. \hyperref[b22]{Collins (1998)}, opined that formal methods are techniques used to model complex systems as mathematical entities. By building a mathematically rigorous model of a complex system, it is possible to verify the system's properties in a more thorough fashion than empirical testing.\par
System engineers can inspect the modeled system architecture to determine whether it is acceptable, but few formal methods exist to aid in the performance of this task \hyperref[b26]{(Rodano \& Giammarcob, 2013)}. In a safety critical system, ambiguity can be extremely dangerous, and one of the primary benefits of the formal approach is the elimination of ambiguity \hyperref[b17]{(Kling, 1994)}.\par
Modelling is one of the ways used in presenting performance evaluation. Heuristics can be applied in determining the good characteristics for performance evaluation. Formal methods can be applied to identify the characteristics of a good system architecture using logical notations. Formal method is the fast approach to identify possible problems in any software architectural design \hyperref[b26]{(Rodano \& Giammarcob, 2013)}.\par
Performance evaluation gives a measure of the service delivered by a system (Jean-Yves \& Boudec, 2010) and performance is one of the most important non-functional aspects of any (hardware or software) system. Performance evaluation comprises of certain techniques such as direct measurements using testbeds, analytical or simulation modeling which can be applied to existing or envisioned systems like computer systems, communication networks, algorithms and protocols  {\ref (Jain, 1991)}. The basic and final goal of the performance evaluation concept is to come to a conclusion, whether the software and system are working in a good condition or satisfactorily. This is can be achieved with formal modelling techniques.\par
Datamining is the discovery of "models" fordata (Leskovec, Rajaraman \& Ullman, 2014). According to Anwaar, Junaid, Raihan, Arjuna, Andrej \& Jon (2016), datamining normally denotes the automation of pattern discovery and prediction from huge volumes of data using Machine Learning (ML) techniques. Datamining can also be used to denote an Online Analytical Processing (OLAP) or Structured Query Language (SQL) queries that entails retrospectively searching a large data base for a specific query. There has been upsurge in availability of information and device connectivity have brought about increase in application of machine learning (which is a sub-domain Artificial Intelligence (AI) in diverse areas (Akinsola, Awodele, Idowu \& Kuyoro, 2020). These areas include applications of Machine Learning (ML) in performance evaluation and verification of software. ML requires application of algorithms for model building using performance metrics. Every performance metric must be considered holistically before choosing an optimal algorithm for predictive analytics (Akinsola, Awodele, Idowu \& Kuyoro, 2020).\par
Formal method axioms can be used in structural evaluation of a software model especially data mining model. The relationships among the various elements of data mining software you be used to evaluate its effectiveness in terms of performance. Formal methods can be used for testing the realization of the entire software against its specification as well as connections between components in order to determine its interoperability.\par
Characteristics heuristics natural language axioms. The axioms symbolizes syntactic checks that can be used in software performance evaluation. Transformation of axioms into formal language notation is essential in performance evaluation of data mining software. CORE and Innoslate are some of the software engineering tools for software performance evaluation.\par
The quality of any software for performance evaluation has three sets of factors which are functionality, engineering, and adaptability. They are also referred to as exterior quality, interior quality and future quality respectively. Formal method functionality features are the exterior qualities such as Correctness, Reliability. Usability and Integrity. The engineering features are Efficiency, Testability, Documentation and Structure while the adaptability features are Flexibility, Reusability and Maintainability II. 
\section[{Literature Review}]{Literature Review}\par
Axioms are statements that we cannot deny without using them in our denial. Axioms are the foundation of all knowledge. When they are well constructed, the transformation of axioms into formal language notation can be a veritable tool in performance evaluation of data mining software. Formal methods axioms can be used in structural evaluation of a software model especially data mining model. CORE I is used for analyzing the axioms. Innoslate is a web-based system modeling tool that is based on the Lifecycle Modeling Language (LML)\par
Model consists of five classes: requirements, activities, connectors, performers, and resources. Resources are data or information that is produced and/or consumed by the system. An activity is an element that transforms inputs into outputs (inputs and outputs are both resources). Performers carry out activities, and physical or logical relationships between performers are known as connectors. Requirements are written specifications for the system (Giammarco, 2012) Markov chains have become an accepted technique for modeling a great variety of situations. Formal methods in computer science as a prominent approach to the rigorous design of computer, communication and software systems. Markov chains, the fundamental performance modeling formalism in use since the early 1900s. The success that has accompanied queuing modeling has largely eliminated the need to set up and solve global balance equations numerically. However, as models become more complex, it is becoming increasing evident that there is place for numerical analysis methods in the modelers' toolbox \hyperref[b29]{(Stewart, 2007)}.\par
Queuing Networks (QNs) have been proved to be a powerful and versatile tool for system performance evaluation and prediction. Queuing networks, a class of stochastic models extensively applied to represent and analyze resource-sharing systems such as communication and computer systems. Product-form queuing networks, allows for defining efficient algorithms to evaluate average performance measures. The main computational algorithms for QNs have been integrated in various software tools for performance modelling and analysis that include user friendly interfaces based on different languages to take into account the particular field of application, e.g., computer networks, computer systems. Basic queuing systems have been defined in queuing theory and applied to analyze congestion systems \hyperref[b5]{(Balsamo \& Marin, 2007)}.\par
Generalized Stochastic Petri Nets (GSPNs), a modeling formalism that can be conveniently used both for the functional verification of complex models of discrete-event dynamic software and systems as well as for their performance and reliability evaluation. The automatic construction of the probabilistic models that underlie the dynamic behaviors of these nets rely on a set of results that derive from the theory of untimed Petri Nets. Petri nets are a powerful tool for the description and the analysis of systems that exhibit concurrency, synchronization and conflicts. There is general consensus that the only means of successfully dealing with large models is to keep them simple by using a "divide and conquer" approach in which the solution of the entire model is constructed on the basis of the solutions of its individual components \hyperref[b4]{(Balbo, 2007)}.\par
Process algebras emerged as a modelling technique for the functional analysis of concurrent systems approximately twenty years ago. Over the last 17 years there have been several attempts to take advantage of the attractive features of this modelling paradigm within the field of performance evaluation. Stochastic Process Algebras (SPA) were first proposed as a tool. Stochastic process algebras and their use in performance modeling, with a focus on the PEPA formalism is highly efficient for evaluation. The compositional modeling capabilities of the formalism and the tools available to support Markov-chain based analysis are good for formal models building (Clark, Gilmore, Hillston, \& Tribastone, 2007). The formality of the process algebra approach allows assigning of a precise meaning to every language expression. This implies that once we have a language description of a given system its behavior can be deduced automatically (Clarke et al., 2007) Performance-oriented notations provide the designer with the capability of building performance aware system models, which can be used in the early development stages to predict the satisfy ability of certain performance requirements as well as to choose Markovian behavioral equivalences with respect to a number of criteria such as their discriminating power, the exactness of the Markov-chain-level aggregations they induce, the achievement of the congruence property, the existence of sound and complete axiomatizations, the existence of logical characterizations, and the existence of efficient verification algorithms can provide satisfactory analysis with respect to certain criteria such as exact aggregation, congruence property , sound and complete axiomatization, logical characteristics and verification complexity \hyperref[b9]{(Bernardo, 2007)}.\par
Probability is an important component in the design and analysis of software and hardware systems. In distributed algorithms electronic coin tossing is used as a symmetry breaker and as a means to derive efficient algorithms, Model checking for both discretetime and continuous-time Markov chains, which deals with algorithms for verifying them against specifications written in probabilistic extensions of temporal logic, including quantitative properties with rewards supports probabilistic modeling such as Probabilistic Symbolic Model (PRISM) checker \hyperref[b18]{(Kwiatkowska, Norman \& Parker, 2007)}.\par
Software performance engineering (SPE) is a systematic, quantitative approach to constructing software systems that meet performance requirements. SPE provides an engineering approach to performance, avoiding the extremes of performance-driven development and "fix-it-later." SPE uses model predictions to evaluate trade-offs in software functions, hardware size, quality of results, and resource requirements. Two SPE models provide the quantitative data for SPE: the software execution model and the system execution model. The software execution model represents key facets of software execution behavior. The model solution quantifies the computer resource requirements for each performance scenario. The system execution model represents computer system resources with a network of queues and servers. The model combines the performance scenarios and quantifies overall resource utilization and consequent response times of each scenario \hyperref[b28]{(Smith, 2007)}. Merits and Demerits of Formal Methods for Performance Evaluation a) Merits It is effectual to write a specification formally rather than writing an informal specification and then translating it.\par
To detect inconsistency and incompleteness, it is efficient to analyze the formal specification as early as possible \hyperref[b24]{(Mona, Amit \& Meenu, 2010)}. Given below are some of the merits of formal methods in software performance evaluation: i. Measure of correctness: The use of formal methods provides a measure of the correctness of a system, as opposed to the current process quality measures. ii. Early defect detection: Formal Methods can be applied to the earliest design artifacts, thereby leading to earlier detection and elimination of design defects. iii. Guarantees of correctness: Formal analysis tools such as model checkers consider all possible execution paths through the system. If there is any possibility of a fault/error, a model checker will find it. In a multithreaded system where concurrency is an issue, formal analysis can explore all possible interleaving and event orderings. This level of coverage is impossible to achieve through testing. iv. Error Prone: Formal description forces the writer to ask all sorts of questions that would otherwise be postponed until coding. This helps to reduce the errors. 
\section[{b) Demerits}]{b) Demerits}\par
Formal methods are generally viewed with suspicion by the professional engineering community  {\ref (Bowen,} {\ref 93)}. Given below are some of the demerits of formal methods in software performance evaluation: 
\section[{i. Expansive}]{i. Expansive}\par
Formal Methods are expense. This is because of the rigor involved, formal methods are always going to be more expensive than traditional approaches to engineering. Also, the tool development cost is high. 
\section[{ii. Limits of Computational Models}]{ii. Limits of Computational Models}\par
While not a universal problem, most formal methods introduce some form of computational model, usually hamstringing the operations allowed in order to make the notation elegant and the system provable. Unfortunately, these design limitations are usually considered intolerable from a developer's perspective.\par
iii. Usability Traditionally, formal methods have been judged on the richness of their descriptive model. That is, 'good' formal methods have described a wide variety of systems, and 'bad' formal methods have been limited in their descriptive capacities. iv. Adaptability SPE activities are not easy to adapt and economical for future environments. So it needs to evolve in order to make SPE adaptable.\par
IV. 
\section[{Conclusion}]{Conclusion}\par
Formal Methods (FM) is a very active research area with a wide variety of methods and mathematical models. There is not available any one method that fulfills all the related needs of building a formal specification. Just like the No Free Lunch theorem is highly essential in the field of machine learning because good number of correctly classified instances in predicting valid disease outcomes using supervised machine learning techniques is not just a function of accuracy (Akinsola, Adeagbo, Awoseyi, Ayomikun, 2019).Performance evaluation of software using formal methods can be carried out using hybridization of machine learning and Multi Criteria Decision Making (MCDM) techniques. MCDM methods can be used to find the optimal classification and regression models in relation to supervised machine learning algorithms (Akinsola, Kuyoro, Awodele \& Kasali, 2019).\par
Researchers and practitioners are continuously working in this area and there by gaining the benefits of using formal methods. Furthermore, formal methods are only part of the solution to the problem related to requirement analysis and success depends crucially on integrating them into a larger process. Formal method axioms are being used in structural evaluation of a software model especially data mining model. Survey of Markovian Behavioral Equivalences supports a merely qualitative analysis, in the sense that it only allows one to establish whether two models pass an arbitrary test in the same way.\par
Generalized Stochastic Petri nets (GSPNs) can be conveniently used for the analysis of complex models of Discrete Event Dynamic Systems (DEDS) and for their performance and reliability evaluation. Classical Process algebra (CPA) can be used to develop models which may be used to calculate performance measures as well as deduce functional properties of the system.\par
Markovian Bisimilarity ?MB, Markovian Testing equivalence ?MT, and Markovian Trace equivalence ?MTr with respect to a number of criteria such as exact aggregation, congruence property , sound and complete axiomatization, logical characteristics and verification complexity can be used to model by taking advantage of symmetries within the model. Stochastic model checking can be used to cover both the theory and practical aspects for two important types of probabilistic models such as discrete-and continuoustime Markov chains.\par
Software Performance Engineering (SPE) should become better integrated into capacity planning. There has been a tremendous amount of research in the SPE field since it was first proposed as a discipline in 1981. The emphasis will change from finding and correcting design flaws to verification and validation that the system performs as expected. The verification and validation can be implemented using predictive analytics with proper application of the best fit machine learning algorithms. Supervised predictive machine learning, ML algorithms require precise accuracy and minimum errors in addition to putting several factors into consideration (Osisanwo, Akinsola, Awodele, Hinmikaiye, Olakanmi \& Akinjobi, 2017) 
\section[{Software Application Gap Analysis}]{Software Application Gap Analysis}\par
Software assessment must be determined in a manner whether business requirements are being met, if not, what steps should be taken to ensure they are met successfully. The following must be considered for critical performance evaluation.\par
1. The natural language axioms deals with first-order predicate logic notation, therefore, it cannot be used for implementing more complex software performance evaluation. 2. The axioms are too generic and might not be robust enough to cope with evaluating certain software classes effectively. Therefore, domain specific axioms should be developed 3. The verification and validation components of the software performance evaluation process should include more analyzer to make it efficient and highly scalable with focus on machine learning. 4. In Markovian Behavioral Equivalences none of the proposals seems to induce an exact aggregation at the Continuous-Time Markov Chains (CTMC) level 5. Markov chains focuses on numerical analysis of modelling but cannot handle novel approaches concerning the special structures in performance evaluation, thus cannot handle complex models. 6. There is need for the development of the solid theoretical framework of model construction and analysis for Generalized Stochastic Petri nets (GSPNs). 7. Determination of the execution probability and the average duration of the computations in the presence of passive transitions is highly is a challenge. Also, the set of logical operators necessary to characterize Markovian behavioral equivalences decreases as the discriminating power of the equivalences decreases. 8. PRISM model checker for stochastic model checking may prove too simplistic for some modelling applications. 9. There is need to extend the quantitative methods to model emerging hardware-software developments, to extend hardware-software measurement technology to support SPE, and to develop interdisciplinary techniques to address the more general definition of performance.\begin{figure}[htbp]
\noindent\textbf{1}\includegraphics[]{image-2.png}
\caption{\label{fig_0}Figure 1 :C}\end{figure}
 \begin{figure}[htbp]
\noindent\textbf{2}\includegraphics[]{image-3.png}
\caption{\label{fig_1}Figure 2 :}\end{figure}
 \begin{figure}[htbp]
\noindent\textbf{}\includegraphics[]{image-4.png}
\caption{\label{fig_2}Global}\end{figure}
  			\footnote{© 2020 Global Journals} 			\footnote{Performance Evaluation of Software using Formal Methods} 		 		\backmatter  			  				\begin{bibitemlist}{1}
\bibitem[Giammarco et al. ()]{b14}\label{b14} 	 		\textit{A Formal Method for Assessing Interoperability using Architecture Model Elements and Relationships},  		 			K Giammarco 		,  		 			G Xie 		,  		 			C A Whitcomb 		.  		2012. 2012.  	 
\bibitem[Rodano and Giammarcob ()]{b26}\label{b26} 	 		‘A Formal Method for Evaluation of a Modeled System Architecture’.  		 			M Rodano 		,  		 			K Giammarcob 		.  	 	 		\textit{Procedia Computer Science}  		2013. 2013. 20 p. .  	 	 (Complex Adaptive Systems. Published by Elsevier B.V) 
\bibitem[Advanced Lectures (2007)]{b8}\label{b8} 	 		\textit{Advanced Lectures},  		May 28-June 2, 2007. 2007. Bertinoro, Italy; Berlin Heidelberg: Springer-Verlag.  	 
\bibitem[Wikipedia ()]{b30}\label{b30} 	 		\textit{Available at},  		 			Wikipedia 		.  		 \url{https://en.wikipedia.org/wiki/Formal\textunderscore methods}  		2017.  	 
\bibitem[Anwaar et al. ()]{b3}\label{b3} 	 		\textit{Big data for development: applications and techniques. Big Data Analytics, 1/2,1-24},  		 			A Anwaar 		,  		 			Q Junaid 		,  		 			R Raihan 		,  		 			S Arjuna 		,  		 			Z Andrej 		,  		 			Jonc 		.  		 \xref{http://dx.doi.org/10.1186/s41044-016-0002-4}{10.1186/s41044-016-0002-4}.  		 \url{http://i.stanford.edu/\textasciitilde ullman/mmds/book.pdf}  		2016.  	 
\bibitem[Bowen and Stavridou ()]{b10}\label{b10} 	 		 			\& Bowen 		,  		 			Stavridou 		.  		\textit{Safety Critical Systems, Formal Methods and Standards},  				1993.  	 
\bibitem[Akinsola et al. (2019)]{b0}\label{b0} 	 		‘Breast Cancer Predictive Analytics Using Supervised Machine Learning Techniques’.  		 			Jide E T Akinsola 		,  		 			Adeagbo 		,  		 			A Moruf 		,  		 			Awoseyi 		,  		 			A Ayomikun 		.  		 \xref{http://dx.doi.org/10.30534/ijatcse/2019/70862019}{10.30534/ijatcse/2019/70862019}.  		 \url{http://www.warse.org/IJATCSE/static/pdf/file/ijatcse70862019.pdfDOI:https://doi.org/10.30534/ijatcse/2019/70862019}  	 	 		\textit{International Journal of Advanced Trends in Computer Science and Engineering}  		 2278-3091.  		November -December 2019. 8  (6)  p. .  	 
\bibitem[Rushby ()]{b27}\label{b27} 	 		\textit{Formal Methods and their Role in the Certification of Critical Systems -SRI -1995},  		 			J Rushby 		.  		1995.  	 
\bibitem[Bernardo and Hillston ()]{b7}\label{b7} 	 		\textit{Formal Methods for Performance Evaluation. 7th International School on Formal Methods for the Design of Computer, Communication and Software Systems},  		 			M Bernardo 		,  		 			J Hillston 		.  		2007. 2007. SFM.  	 
\bibitem[Collins ()]{b22}\label{b22} 	 		\textit{Formal Methods. Carnegie Mellon University, 18-849b Dependable Embedded Systems},  		 			Michael Collins 		,  		 			M 		.  		 \url{https://users.ece.cmu.edu/\textasciitilde koopman/des\textunderscore s99/formal\textunderscore methods/}  		1998. 1998.  	 
\bibitem[Mona et al. (2010)]{b24}\label{b24} 	 		‘Formal Methods: Benefits, Challenges and Future Direction’.  		 			B Mona 		,  		 			M Amit 		,  		 			D Meenu 		.  	 	 		\textit{Journal of Global Research in Computer Science © JGRCS}  		2010. 2010. May 2013. 4  (5)  p. .  	 
\bibitem[Lamsweerde ()]{b19}\label{b19} 	 		‘Formal Specification: A Roadmap’.  		 			A V Lamsweerde 		.  	 	 		\textit{Proceedings of the Conference on the Future of Software Engineering},  				 (the Conference on the Future of Software Engineering)  		2000. 2000. ACM. p. .  	 
\bibitem[Miller and Srivas ()]{b23}\label{b23} 	 		\textit{Formal Verification of the AAMP5 Microprocessor},  		 			\& Miller 		,  		 			Srivas 		.  		1995.  	 
\bibitem[Balbo ()]{b4}\label{b4} 	 		‘Introduction to Generalized Stochastic Petri Nets’.  		 			G Balbo 		.  	 	 		\textit{SFM 2007},  		LNCS  		 (Torino, Italy; Berlin Heidelberg)  		2007. 2007. 2007. Springer-Verlag. 185 p. .  	 	 (Universit`a di Torino) 
\bibitem[Smith ()]{b28}\label{b28} 	 		‘Introduction to Software Performance Engineering: Origins and Outstanding Problems. Performance Engineering Services’.  		 			C U Smith 		.  	 	 		\textit{SFM 2007},  		LNCS  		 (Santa Fe, NM; Berlin Heidelberg)  		2007. 2007. 2007. Springer-Verlag. 87504 p. .  	 
\bibitem[Kling ()]{b17}\label{b17} 	 		 			R Kling 		.  		\textit{Systems Safety, Normal Accidents and Social Vulnerability},  				1994.  	 
\bibitem[Leskovec et al. ()]{b20}\label{b20} 	 		 			J Leskovec 		,  		 			A Rajaraman 		,  		 			D J \&ullman 		.  		\textit{Mining of Massive Datasets},  				2014.  	 
\bibitem[Boudec ()]{b15}\label{b15} 	 		\textit{Performance Evaluation of Computer and Communication Systems},  		 			Jean-Yves \& Boudec 		,  		 			L 		.  		2010. 2010. Lausanne, Switzerland: EPFL Press.  	 
\bibitem[Akinsola et al. ()]{b16}\label{b16} 	 		‘Performance Evaluation of Supervised Machine Learning Algorithms Using Multi-Criteria Decision Making Techniques’.  		 			J E T Akinsola 		,  		 			S O Kuyoro 		,  		 			O \& F A Awodele 		,  		 			Kasali 		.  	 	 		\textit{International Conference on Information Technology in Education and Development (ITED) Proceedings},  				2019. p. .  	 
\bibitem[Stewart ()]{b29}\label{b29} 	 		‘Performance Modelling and Markov Chains’.  		 			W J Stewart 		.  	 	 		\textit{SFM 2007},  				 (Raleigh, NC 27695, USA; Berlin Heidelberg)  		2007. 2007. Springer-Verlag. 4486 p. .  		 			Department of Computer Science, North Carolina State University 		 	 
\bibitem[Balsamo and Marin ()]{b5}\label{b5} 	 		\textit{Queuing Networks. Dipartimento di Informatica Universit`a Ca' Foscari di Venezia Via Torino},  		 			S \& Andrea Balsamo 		,  		 			A Marin 		.  		2007. 155 p. 30172.  	 
\bibitem[Almeida et al. ()]{b2}\label{b2} 	 		\textit{Rigorous Software Development, A Practical Introduction to Program Verification. Series: Undergraduate Topics in Computer Science},  		 			J B Almeida 		,  		 			M J Frade 		,  		 			J S Pinto 		,  		 			Melo De 		,  		 			S Sousa 		.  		2011. 2011. Springer Verlag.  	 	 (1st Edition. 52 illus. Soft cover) 
\bibitem[Melo De Sousa ()]{b21}\label{b21} 	 		\textit{Rigorous Software Development: An introduction},  		 			S Melo De Sousa 		.  		2011.  	 
\bibitem[Bowen and Hinchey ()]{b11}\label{b11} 	 		‘Seven More Myths of Formal Methods’.  		 			J P Bowen 		,  		 			M G Hinchey 		.  	 	 		\textit{IEEE Software}  		1995. 1995. 12 p. .  	 
\bibitem[SFM 2007 ()]{b6}\label{b6} 	 	 	 		\textit{SFM 2007},  		LNCS  		 (Venezia Mestre, Italy; Berlin Heidelberg)  		2007. 2007. Springer-Verlag. 4486 p. .  	 
\bibitem[Akinsola et al. (2020)]{b1}\label{b1} 	 		‘SQL Injection Attacks Predictive Analytics Using Supervised Machine Learning Techniques’.  		 			Jide E T Akinsola 		,  		 			Awodele 		,  		 			; Oludele 		,  		 			Sunday A Idowu 		,  		 			Kuyoro 		,  		 			O Shade 		.  		 \xref{http://dx.doi.org/10.7753/IJCATR0904.1004}{10.7753/IJCATR0904.1004}.  		 \url{https://10.7753/IJCATR0904.1004}  	 	 		\textit{International Journal of Computer Applications Technology and Research}  		 -2319- 8656.  		2020. April, 2020. 9  (04)  p. .  	 
\bibitem[Kwiatkowska et al. ()]{b18}\label{b18} 	 		‘Stochastic Model Checking’.  		 			M Kwiatkowska 		,  		 			G Norman 		,  		 			D Parker 		.  	 	 		LNCS  		2007. 2007. 2007. 2007. Springer-Verlag. 4486 p. .  		 			School of Computer Science, University of Birmingham Edgbaston 		 	 
\bibitem[Clark et al. ()]{b12}\label{b12} 	 		‘Stochastic Process Algebras. LFCS, School of Informatics’.  		 			A Clark 		,  		 			S Gilmore 		,  		 			J Hillston 		,  		 			M Tribastone 		.  	 	 		\textit{SFM 2007},  				 (Berlin Heidelberg)  		2007. 2007. 2007. Springer-Verlag. 4486 p. .  		 			University of Edinburgh 		 	 
\bibitem[Osisanwo et al. ()]{b13}\label{b13} 	 		‘Supervised Machine Learning Algorithms: Classification and Comparison’.  		 			F Y Osisanwo 		,  		 			J E T Akinsola 		,  		 			O Awodele 		,  		 			J O Hinmikaiye 		,  		 			O Olakanmi 		,  		 			J Akinjobi 		.  		 \xref{http://dx.doi.org/10.14445/22312803/IJCTT-V48P126}{10.14445/22312803/IJCTT-V48P126}.  		 \url{https://doi:10.14445/22312803/IJCTT-V48P126}  	 	 		\textit{International Journal of Computer Trends and Technology}  		2017. 48.  	 
\bibitem[Rechtin ()]{b25}\label{b25} 	 		‘The Art of Systems Architecting’.  		 			E Rechtin 		.  	 	 		\textit{IEEE Spectrum}  		1992. 1992. 29 p. .  	 
\bibitem[Bernardo ()]{b9}\label{b9} 	 		‘Universit`a di Urbino "Carlo Bo" -Italy Istituto di Scienze e Tecnologie dell'Informazione’.  		 			M Bernardo 		.  	 	 		\textit{SFM 2007},  		LNCS  		 (Berlin Heidelberg)  		2007. 2007. 2007. Springer-Verlag. 4486 p. .  	 	 (A Survey of Markovian Behavioral Equivalences) 
\end{bibitemlist}
 			 		 	 
\end{document}
