<?xml version="1.0" encoding="UTF-8"?>
<TEI xml:space="preserve" xmlns="http://www.tei-c.org/ns/1.0" 
xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" 
xsi:schemaLocation="http://www.tei-c.org/ns/1.0 https://raw.githubusercontent.com/kermitt2/grobid/master/grobid-home/schemas/xsd/Grobid.xsd"
 xmlns:xlink="http://www.w3.org/1999/xlink">
	<teiHeader xml:lang="en">
		<fileDesc>
			<titleStmt>
				<title level="a" type="main">Formalizing and Verifying Natural Language System Requirements using Petri Nets and Context based Reasoning</title>
			</titleStmt>
			<publicationStmt>
				<publisher/>
				<availability status="unknown"><licence/></availability>
			</publicationStmt>
			<sourceDesc>
				<biblStruct>
					<analytic>
						<author>
							<persName><forename type="first">Aishwarya</forename><surname>Chhabra</surname></persName>
							<email>aishwarya.chhabra@tcs.com</email>
							<affiliation key="aff0">
								<orgName type="institution">TCS Innovation Labs</orgName>
								<address>
									<settlement>Gurgaon</settlement>
									<country key="IN">India</country>
								</address>
							</affiliation>
						</author>
						<author>
							<persName><forename type="first">Amit</forename><surname>Sangroya</surname></persName>
							<email>amit.sangroya@tcs.com</email>
							<affiliation key="aff0">
								<orgName type="institution">TCS Innovation Labs</orgName>
								<address>
									<settlement>Gurgaon</settlement>
									<country key="IN">India</country>
								</address>
							</affiliation>
						</author>
						<author>
							<persName><forename type="first">C</forename><surname>Anantaram</surname></persName>
							<email>c.anantaram@tcs.com</email>
							<affiliation key="aff0">
								<orgName type="institution">TCS Innovation Labs</orgName>
								<address>
									<settlement>Gurgaon</settlement>
									<country key="IN">India</country>
								</address>
							</affiliation>
						</author>
						<title level="a" type="main">Formalizing and Verifying Natural Language System Requirements using Petri Nets and Context based Reasoning</title>
					</analytic>
					<monogr>
						<imprint>
							<date/>
						</imprint>
					</monogr>
					<idno type="MD5">0018BD4C22F9685F77F501FF7614050A</idno>
				</biblStruct>
			</sourceDesc>
		</fileDesc>
		<encodingDesc>
			<appInfo>
				<application version="0.7.2" ident="GROBID" when="2023-03-25T04:28+0000">
					<desc>GROBID - A machine learning software for extracting information from scholarly documents</desc>
					<ref target="https://github.com/kermitt2/grobid"/>
				</application>
			</appInfo>
		</encodingDesc>
		<profileDesc>
			<abstract>
<div xmlns="http://www.tei-c.org/ns/1.0"><p>Natural language descriptions are generally used to describe requirements in reactive systems. Translating the natural language requirements to a more formal specification is a challenging task. One possible approach to handle complex natural language requirements is to convert them to an intermediary formal representation. This intermediate representation is further converted into a more formal representation such as EDT (Expressive Decision Tables). In this paper, we use Petri nets in combination with domain based context reasoning as a tool to model natural language requirements. We have also built a tool, NatEDT, to generate EDT specifications. In a case study, consisting of natural language requirements across three domains, our experimental results show that Petri nets provide an efficient way of formalizing natural language requirements.</p></div>
			</abstract>
		</profileDesc>
	</teiHeader>
	<text xml:lang="en">
		<body>
<div xmlns="http://www.tei-c.org/ns/1.0"><head n="1">Introduction</head><p>With the rapid growth of the internet of things (IoT), smart homes, smart cars, smart factories have become a reality. These smart systems are kind of reactive systems that interact via various sensors. It becomes a challenging task for system designers to conceptualize systems that can take complex natural language sentences as an input and test/verify the requirement. Table <ref type="table" target="#tab_0">1</ref> shows some examples of natural language specifications from multiple domains of reactive systems.</p><p>The NL requirements can belong to a system as simple as switching on a light or as complex as control a fire detection system remotely. It is important for system designers to have an engineering approach to formalize NL requirement specifications. In this paper, we focus on system requirements that are primarily the descriptions of how a system (i.e. Smart Home/Automobile/IoT based system) is expected to perform in a real environment. An example of such a description in an automobile domain is as follows. "If the ignition is on for more than 45 seconds, and seat belt is not engaged then alarm should beep". In this example, alarm system should beep; if the ignition is on and the seat belt is not engaged.</p><p>Many-a-times the specifications of such systems are specified in natural language sentences by designers. At times Automobile Domain: If the ignition is on, and switch 1 is on for 2 seconds then operation 1 becomes required. Turn Indicator System: When the turn indicator lever becomes left position, and the emergency flashing is off, then the flashing mode component shall assign left flashing to the flashing mode, set 0 at the flashing timer. Air Conditioning Domain: When swing mode is vertical, and operation mode is cooling, then operation type becomes high speed.</p><p>such specifications also tend to change for different system configurations and also over a period of time. In order to make it easier for system designers to define such specifications and update them, it is important to have a way to convert the specifications from natural language sentences into formal specifications. In general, requirements broadly consists of two parts: the condition part and the action part. In our approach we take NL requirement specification as an input and produce Expressive decision tables as the final output. EDT is a formal way of representing the NL specification which can be tested and verified <ref type="bibr" target="#b4">[Venkatesh et al., 2014]</ref>. EDT is a regular expression based, tabular format notation for reactive systems. An example of EDT is as follows (See Table <ref type="table" target="#tab_1">2</ref>).</p><p>For reactive systems, EDT representations can be easily verified for functional testing in comparison to NL specifications. This is because of the fact that natural language specifications can be ambiguous or sometimes incomplete. System designers sometimes use natural language as it can be easily written without getting into the complexity of the problem. However, to verify these reactive systems, we need test cases, and it is better to generate test cases using a formal language. Hence, it necessitates the automation of natural language to a formal language in order to bridge the gap between natural To this end, we designed a tool called NatEDT (Natural Language to EDT) to translate the natural language specifications to formal notation using Petri nets as an intermediary and verification mechanism. Our Approach consists of several steps consisting of pre-processing, NL parsing, intermediary Petri net representation and final output as EDT. In addition to this, we have an additional step of verification that helps to test the properties like completeness and consistency of requirements. The overall approach is domain agnostic and can be easily adapted to new domains.</p><p>The remainder of this paper is structured as follows. Section 3 provides a small introduction to preliminaries which are essential for our work. Section 4 presents the proposed architecture of the system that takes natural language requirements as an input and provides a formal specification as an output. Then section 5 discusses the experimental evaluation. Section 2 offers an overview of the existing state of art approaches that focus on formalizing natural language requirement specifications. Finally, in section 6, this work ends up with some conclusions and an outlook of our future work in this area.</p></div>
<div xmlns="http://www.tei-c.org/ns/1.0"><head n="2">Related Work</head><p>We classify the existing approaches into two categories.</p><p>Approaches using Restrictive Natural Language One way is to restrict the language used in writing the requirements specifications to make semantic parsing easier <ref type="bibr" target="#b5">[Yan et al., 2015]</ref>. Gutavo et al. use the Control Natural Language(CNL) for writing the specifications and have also defined a grammar for that CNL structure to do Syntactic Analysis <ref type="bibr" target="#b0">[Carvalho et al., 2014]</ref>. They also talk about the trade off between removing restrictions from the grammar and automation extent. They say that they aim at fully automating the formalizing process by restricting the language and providing a fixed format of the specifications. Since NL is controlled, a lot of manual effort is required in converting the Specification to that controlled format. <ref type="bibr" target="#b0">Böschen et al. [Böschen et al., 2016]</ref> uses a preprocessing approach to enrich the natural language requirements using a knowledge base. In this context, our approach is complementary to their work since we also use a domain ontology to contextualize the natural language requirements.</p><p>Approaches using Less Restrictive Natural Language Less restrictive NL specifications are more natural in comparison to restrictive approaches; hence making it easier for users to write these requirements. Bajwa et al. propose an approach of scanning the specifications for relevant relationships and extracting them <ref type="bibr" target="#b0">[Bajwa et al., 2012;</ref><ref type="bibr" target="#b0">2010]</ref>. They also use intermediary models from which they extract the final concepts. However, their approach is primarily based on information extraction. Other NL processing techniques such as parsing, exploiting the use of patterns, regular expressions, and rules, etc. can provide extraction of concepts and relationships from the unrestricted natural language requirement specification. Validation of the output model from the business specification must be performed which can be a laborious for large specifications.</p><p>Our approach is based upon parsing that reduces the manual effort of validating the output that is involved in approached based on information extraction <ref type="bibr" target="#b0">[Ghosh et al., 2016]</ref>. Shalini et al. proposed ARSENAL which works for less restrictive grammar but our approach verifies for the correctness using domain ontology. In this approach complete parsing is done and its semantic interpretation is done in context of the domain knowledge. Selvet et al. also takes an advantage of parsing but their approach is different in all respects as they are using SBVR (Semantics of Business Vocabulary and Business Rules) for semantic understanding <ref type="bibr" target="#b4">[Selway et al., 2015]</ref>. Sadoun et al. make the use of extracting rules automatically acquired by a training corpus, and identify concepts using a domain ontology <ref type="bibr" target="#b4">[Sadoun et al., 2013]</ref>.</p><p>We also use domain knowledge in the form of ontology to validate all the identified Variables and its values. Petri nets have been used as a verification mechanism in various domains <ref type="bibr" target="#b0">[Lee et al., 2001;</ref><ref type="bibr" target="#b4">Sarmiento et al., 2015]</ref>. Our approach is more promising as it gives an additional step of verification. Using Petri Nets as an intermediary model gives us a more robust verification mechanism and visual representation. The primary advantages of our approach over the state of art approaches is that requirements can be in less restrictive natural language. We use a domain dictionary that allows to write NL requirements using a rich vocabulary. Use of Petri nets as an intermediary helps in validation of NL specification and also preserving the context. Additionally, NatEDT has a verification process for formal verification of NL specifications.</p></div>
<div xmlns="http://www.tei-c.org/ns/1.0"><head n="3">Preliminaries</head></div>
<div xmlns="http://www.tei-c.org/ns/1.0"><head n="3.1">Expressive Decision Tables (EDT)</head><p>An EDT specification <ref type="bibr" target="#b4">[Venkatesh et al., 2014]</ref> consists of one or more tables where the column headers specify the input and output ports and the rows specify the relationship between input and output values. Each cell in a row consists of a regular expression that is used to match input streams at that port. Input values arrive as a stream at input ports at discrete time units and output values are generated as a stream at output ports at discrete time units. Example of EDT is shown in table <ref type="table" target="#tab_1">2</ref>, where "in" stands for input and "out" stands for output.</p></div>
<div xmlns="http://www.tei-c.org/ns/1.0"><head n="3.2">Ontology</head><p>In the context of knowledge sharing, the term ontology is used to mean a specification of a conceptualization. That is, an ontology is a description of the concepts and relationships that can exist for an agent or a community of agents. This definition is consistent with the usage of ontology as set-ofconcept-definitions, but more general. And it is certainly a different sense of the word than its use in philosophy. We are using domain ontology which covers the concepts and their relationships with its attributes and other values. We are using Protege to construct the ontology in OWL format <ref type="bibr" target="#b2">[Musen, 2015]</ref>.</p><p>Domain ontology helps us specialize the approach to a particular domain which will help in fetching better results. We are using ontology for checking the identified concepts to Tenth International Workshop Modelling and Reasoning in Context (MRC) -13.07.2018 -Stockholm, Sweden check if the concepts extraction does not give incorrect concepts. The verified concepts are processed further and the remaining concepts which do not belong to the domain are dropped. It also helps us identify the correct relationships of the values and the variables.</p></div>
<div xmlns="http://www.tei-c.org/ns/1.0"><head n="3.3">Petri Nets</head><p>Petri nets, also known as Place/Transition Nets, are used to verify work flows. Petri nets are classical models of concurrency, non-determinism, and control flow, first proposed by Carl Adam Petri in 1962. It is a collection of arcs connecting places and transitions. Places refer to the current state of the system whereas transitions are the events that take place and may cause a change in the state of the system. Places may hold tokens which enable the transitions and eventually the transition gets fired, then the tokens are distributed as per the weight given on the arcs. Places of Petri nets usually represent states or resources in the system while transitions model the activities of the system. Petri nets are bipartite graphs and provide an elegant and mathematically rigorous modeling framework for discrete event dynamically systems. Petri nets are a simple but effective method of analysing manufacturing systems <ref type="bibr" target="#b1">[Murata, 1989;</ref><ref type="bibr" target="#b4">van der Aalst, 1998</ref>].  Figure <ref type="figure" target="#fig_2">2</ref> represents the overall architecture. System designers specify the requirement in natural language. First, we perform syntactic analysis that involves POS tagging, chunking, dependency parsing. Thereafter, we perform semantic analysis using semantic parsing techniques. We make use of a domain ontology to identify and confirm the context for a given specification. Thereafter, Petri nets are used for verification of NL specification. The output of this is a formal EDT that can be further processed for test case generation <ref type="bibr" target="#b4">[Venkatesh et al., 2016]</ref>.</p><p>We designed a tool NatEDT, that takes a natural language sentence as an input and generates an equivalent EDT specification and preserves the original context. The current version of the developed prototype not only generates corresponding formal specification but also verifies the NL specifications. The overall workflow of NatEDT consist of following main steps:</p></div>
<div xmlns="http://www.tei-c.org/ns/1.0"><head n="4.1">Preprocessing</head><p>Each system requirement consists of mainly two parts : condition clause and action clause. In preprocessing, the first step is to split the system requirement based on its syntactic structure. The specifications when written in natural language might make use of synonyms of domain specific terms (terms present in domain ontology) instead of directly using them.</p><p>To overcome this we assume that we have a domain dictionary built by domain experts. Using the domain dictionary, synonyms of the domain specific words are replaced with actual domain specific words. For example: For a given NL specification "If ignition is ON, and switch 1 is ON for 2 seconds then operation 1 becomes REQ." , this will be changed to "If IGN is ON, and SW 1 is ON for 2 seconds then OP 1 becomes REQ.". Since in this domain we consider n-gram switch 1 as one domain term so we replace it with SW 1. Moreover, we have some general n-grams like greater than, less than or equal to. These are are replaced with greater than, less than or equal to, respectively.</p></div>
<div xmlns="http://www.tei-c.org/ns/1.0"><head n="4.2">Extraction of Domain Variables</head><p>In requirement specifications, both the condition clause and action clause have some variables and values associated to these variables. We use term input variables for the terms used in conditional clause and output variables for the terms used in action clause. Extracting these variables from the requirement requires an intricate approach, which is described underneath:</p></div>
<div xmlns="http://www.tei-c.org/ns/1.0"><head>Dependency Parsing</head><p>We use Stanford CoreNLP dependency parser for dependency parsing, which gives us a set of triples (dependent, dependency, governor) <ref type="bibr" target="#b0">[Manning et al., 2014]</ref>. For Example: (IGN, nsubj, ON) which means IGN is is related to ON and is the nominal subject for ON. We parse our specification using this Stanford typed dependency parser and get a list of such sets with various dependencies <ref type="bibr" target="#b0">[Marneffe et al., 2006]</ref>. Now let us consider the given example from general automobile domain which has time attributes also. "If IGN is ON, and SW1 is ON for 2 seconds". Figure <ref type="figure" target="#fig_3">3</ref> represents the dependency tree for this specification.</p></div>
<div xmlns="http://www.tei-c.org/ns/1.0"><head>Semantic Analysis and Validation using Ontology</head><p>Now we have all the dependencies, we can also call them grammatical relationships. We need to make sure that while  mapping them to the EDT, we don't lose the context of the specification as these are general grammar relationships. So for all the variables (concepts), we have some attributes associated to them like -value, type, time, modifier. We define some rules associated with the dependencies to fill the slots for these attributes. Using these types of rules we preserve the context of the original requirement while modeling Petri nets and generating formal EDT specifications.</p><p>For example: (SW 1, nsubj, ON) we get SW 1 is the variable and and ON is its value. We can validate the semantic relationship between SW 1 and ON using a domain ontology so that the context is preserved. (2, nummod, seconds) and (seconds , nmod:for, ON) together helps fill us the slot for time attribute. In case of "type" attribute we have two options numeric or non-numeric. For variables like voltage, timer, etc for which the value will always be numeric are categorized in that category and remaining falls into another category. We extract that using POS tags of the values. Last attribute remaining is the modifier which has the values of type greater than, less than, greater than or equal to, equal to, etc. In this example absence of any relation like this implies 'equal to'.</p></div>
<div xmlns="http://www.tei-c.org/ns/1.0"><head n="4.3">Deriving Petri Nets Representations</head><p>In this step we derive Petri net based intermediate representation from the natural language requirement. To model this information into Petri nets we use python SNAKES library <ref type="bibr">[Pommereau, 2008;</ref><ref type="bibr">2015]</ref>. We assign each variable a place. The values of the variables are considered as tokens.</p><p>The expression which satisfies the condition is given at the arcs. When the token fired satisfies the expression on the arcs, transition assigns tokens to the output place. Example : "If IGN is ON, and SW 1 is ON for 2 seconds then OP 1 becomes REQ.". In this step we can fire tokens and visualize the work flow of the requirement specification. Figure <ref type="figure" target="#fig_5">4</ref> shows the network before and after firing of tokens.</p></div>
<div xmlns="http://www.tei-c.org/ns/1.0"><head n="4.4">Generating EDT Specification</head><p>The last step is generation of EDT specifications. As initially described, EDT is in tabular format so we use python libraries like pandas to create a table for the specification. As by now we have identified the concepts and its attributes, and have also validated them in the above steps. We can map it to the EDT format. The places in the Petri nets with the tokens denotes the values at the current state of the system so we can consider places as the column names, where input place will be represented with a prefix 'in' and output variables 'out'. The tokens will be represented as the values in the corresponding rows. Figure <ref type="figure" target="#fig_3">3</ref> shows the table generated for the given example.</p></div>
<div xmlns="http://www.tei-c.org/ns/1.0"><head n="4.5">Verifying Specifications for Contextual Inconsistencies</head><p>We are verifying the extracted domain variables and the values associated to them using an ontology in the transformation process itself. We have added an additional verification step to to the tool which verifies the other requirements   given to check their consistency with the existing requirements. We process a finite number of specifications S (where S = S 1 , S 2 , S 3 , ...S n ) as explained in the above sections and store the information extracted at each step in a file. When a user provides a new input condition (C), it is processed as explained in previous sections. The information extracted from C is matched to the information extracted for specifications (S 1 , S 2 , S 3 , ...S n ) using the verification algorithm which returns complete specification with a Petri net for the given input conditions if an exact match is found. If the exact match is not found it looks for the best match which refers to the one with the highest number of matching input conditions and returns the Petri net and table stored for those specifications.</p><p>For Example: We originally had a specification in set S : "If screen is unlock and power button is pressed for less than 1 second and released, then turn screen to lock". User describes an input condition as: "If screen is unlock and power button is pressed for less than 3 second and released", the tool process this condition and extract two input variables: SCREEN having a value UNLOCK and POWER BUTTON having a value PRESSED for less than 3s and then changes to RELEASED. The verification algorithm couldn't find an exact match in set S, hence looks for the best match highlighting the differences. In this example, it highlights the time attribute is different from the existing best match for the given input. Thereafter, it provides user an additional option to either correct if it was an error or add it as a new requirement specification in the set S by providing the output action for the corresponding input.</p></div>
<div xmlns="http://www.tei-c.org/ns/1.0"><head n="5">Experimental Evaluation</head><p>NatEDT tool was tried on two different set of requirements from automobile domain (Turn Indicator Systems (17 requirements) and another automobile sample set <ref type="bibr" target="#b4">[Venkatesh et al., 2014]</ref> (29 requirements). We also tested toy examples from Air Conditioner domain (See table <ref type="table" target="#tab_7">5</ref>). We tested on different domains to test the adaptability of the approach on different domains and we realized that the approach is generic. To adapt to different domains one need to have external domain dictionary for preprocessing and domain ontology for verification of those specifications. Our evaluation criteria was based upon calculating the precision and recall. We calculated the total number of concepts that need to be identified in each sample set and then the variables which were correctly identified, incorrectly identified, and the missed concepts. The largest requirement in english was composed of 48 words and the smallest sentence was composed of 12 words. The TIS sample was mostly state based examples and the other set had some state based as well as examples having time and stream of inputs. The results are compiled in table 4. We get a precision of 94.36% and a recall of 91.78% in automobile domain. Though we cannot compare our results with any other work as the formal notation and approach used in our paper is quite different than the formal notations and approaches in prior work. Our results are quite promising for the transformation to a relatively new formal notation.</p></div>
<div xmlns="http://www.tei-c.org/ns/1.0"><head n="6">Conclusions and Future Work</head><p>To this end, a tool called NatEDT is developed that takes a natural language sentence as an input and generates an EDT specification. We make use of domain knowledge in the form of dictionary and ontology to preserve the context in NL specification. We are also able to verify the new NL requirements based on the existing requirements for its consistency and completeness. In the future, this work could be extended for robust verification and validation of the requirements in the system.</p><p>Tenth International Workshop Modelling and Reasoning in Context (MRC) -13.07.2018 -Stockholm, Sweden   </p></div><figure xmlns="http://www.tei-c.org/ns/1.0" xml:id="fig_0"><head></head><label></label><figDesc>Definition 3.1. Petri Nets[Petri, 1962]   A Petri net is a four-tuple (P, T, IN, OU T ) where P = p 1 , p 2 , p 3 , ...p n is a finite set of places T = t 1 , t 2 , t 3 , ...t n is a finite set of transitions IN : is an input function that defines directed arcs from places to transitions, and OU T : is an output function that defines directed arcs form transitions to places.Graphically places are represented by circles and transitions represented by horizontal or vertical bars (See Figure1). If IN (p i , t j ) = k, where k &gt; 1 is an integer, a directed arc from place p i to transition t j is drawn with the label k. If k = 1 we include an unlabeled arc and if k = 0 then no arc is drawn.</figDesc></figure>
<figure xmlns="http://www.tei-c.org/ns/1.0" xml:id="fig_1"><head>Figure</head><label></label><figDesc>Figure 1: A simple example of Petri net</figDesc><graphic coords="3,62.00,496.59,226.88,109.29" type="bitmap" /></figure>
<figure xmlns="http://www.tei-c.org/ns/1.0" xml:id="fig_2"><head>Figure 2 :</head><label>2</label><figDesc>Figure 2: Overview of System Architecture</figDesc><graphic coords="4,103.03,53.84,404.67,302.14" type="bitmap" /></figure>
<figure xmlns="http://www.tei-c.org/ns/1.0" xml:id="fig_3"><head>Figure 3 :</head><label>3</label><figDesc>Figure 3: Dependency Graph for NL Specification</figDesc></figure>
<figure xmlns="http://www.tei-c.org/ns/1.0" xml:id="fig_5"><head>Figure 4 :</head><label>4</label><figDesc>Figure 4: Before and After Firing of Tokens</figDesc></figure>
<figure xmlns="http://www.tei-c.org/ns/1.0" type="table" xml:id="tab_0"><head>Table 1 :</head><label>1</label><figDesc>Example of natural language specifications</figDesc><table /></figure>
<figure xmlns="http://www.tei-c.org/ns/1.0" type="table" xml:id="tab_1"><head>Table 2 :</head><label>2</label><figDesc>Example of EDT (Expressive Decision Table)</figDesc><table><row><cell>in IGN ON {&gt; 45s}</cell><cell>in SEAT BELT NOT ENGAGED</cell><cell>out ALARM BEEP</cell></row></table></figure>
<figure xmlns="http://www.tei-c.org/ns/1.0" type="table" xml:id="tab_2"><head>Requirements in Natural Language Example</head><label></label><figDesc>Tenth International Workshop Modelling and Reasoning in Context (MRC) -13.07.2018 -Stockholm, Sweden : "When power saving mode is on, swing mode is off, the controller shall assign off to ventilation function"</figDesc><table><row><cell>Syntactic</cell></row><row><cell>Analysis using</cell></row><row><cell>NLP</cell></row><row><cell>techniques</cell></row></table><note>1 System</note></figure>
<figure xmlns="http://www.tei-c.org/ns/1.0" type="table" xml:id="tab_3"><head>Formal Expressive Decision Tables (EDT) in power_saving_mode in swing_mode out ventilation_function</head><label></label><figDesc></figDesc><table><row><cell>Semantic</cell><cell>Domain</cell><cell>Petri nets</cell></row><row><cell>Analysis</cell><cell>Ontology</cell><cell>Based</cell></row><row><cell>Using</cell><cell>Based Context</cell><cell>Verification</cell></row><row><cell>Semantic</cell><cell>Validation</cell><cell></cell></row><row><cell>Parsing</cell><cell></cell><cell></cell></row><row><cell>on</cell><cell>off</cell><cell>off</cell></row></table></figure>
<figure xmlns="http://www.tei-c.org/ns/1.0" type="table" xml:id="tab_4"><head></head><label></label><figDesc>Tenth International Workshop Modelling and Reasoning in Context (MRC) -13.07.2018 -Stockholm, Sweden</figDesc><table><row><cell></cell><cell></cell><cell></cell><cell></cell><cell></cell><cell cols="2">conj:and</cell><cell></cell><cell></cell><cell></cell><cell></cell><cell></cell></row><row><cell></cell><cell>dep</cell><cell></cell><cell></cell><cell></cell><cell></cell><cell></cell><cell></cell><cell></cell><cell cols="2">nmod:for</cell><cell></cell></row><row><cell></cell><cell></cell><cell>nsubj</cell><cell></cell><cell>cc</cell><cell></cell><cell></cell><cell>nsubj</cell><cell></cell><cell></cell><cell>case</cell><cell></cell></row><row><cell></cell><cell></cell><cell>cop</cell><cell>punct</cell><cell></cell><cell></cell><cell></cell><cell>cop</cell><cell></cell><cell></cell><cell>nummod</cell><cell></cell></row><row><cell>LS</cell><cell>NNP</cell><cell>VBZ</cell><cell>NNP</cell><cell>,</cell><cell>CC</cell><cell>NN</cell><cell>VBZ</cell><cell>NNP</cell><cell>IN</cell><cell>CD</cell><cell>NNS</cell></row><row><cell>If</cell><cell>IGN</cell><cell>is</cell><cell>ON</cell><cell>,</cell><cell>and</cell><cell>SW1</cell><cell>is</cell><cell>ON</cell><cell>For</cell><cell>2</cell><cell>seconds</cell></row></table></figure>
<figure xmlns="http://www.tei-c.org/ns/1.0" type="table" xml:id="tab_5"><head>Table 3 :</head><label>3</label><figDesc>EDT for the representative example</figDesc><table><row><cell>in IGN ON</cell><cell>in SW 1 ON</cell><cell>out OP 1 REQ</cell></row></table></figure>
<figure xmlns="http://www.tei-c.org/ns/1.0" type="table" xml:id="tab_6"><head>Table 4 :</head><label>4</label><figDesc>Precision and Recall for various domains</figDesc><table><row><cell>Turn Indica-tor System Automobile Air Condi-tioning</cell><cell># Samples Recall % Precision% 76 85.52% 100% 49 91.78% 94.36% 17 100% 100%</cell></row></table></figure>
<figure xmlns="http://www.tei-c.org/ns/1.0" type="table" xml:id="tab_7"><head>Table 5 :</head><label>5</label><figDesc>Examples of Natural Language Specification and their corresponding EDTs</figDesc><table><row><cell>1</cell><cell>If Mist Remover Switch is on and Mist Remover controller is NO req then Mist Remover Request becomes on and Mist remover relay is on.</cell><cell>in Mist Remover SW ON</cell><cell>in Mist Remover Ctrl NO REQ</cell><cell>out Mist Remover Request ON</cell><cell>out Mist Remover Relay ON</cell></row><row><cell>2</cell><cell>If Mist Remover Switch is off and Mist Remover controller is NO req then Mist Remover Request becomes off and Mist remover relay is off.</cell><cell>in Mist Remover SW OFF</cell><cell>in Mist Remover Ctrl NO REQ</cell><cell>out Mist Remover Request OFF</cell><cell>out Mist Remover Relay OFF</cell></row><row><cell>3</cell><cell>If alarm is ON, and panicsw is pressed for more than 3 seconds and released then the flash should be NO REQ, and alarm should be OFF.</cell><cell>in alarm ON</cell><cell>in panicSw pressed &gt; 3s re-leased</cell><cell>out flash NO REQ</cell><cell>out alarm OFF</cell></row></table></figure>
		</body>
		<back>
			<div type="references">

				<listBibl>

<biblStruct xml:id="b0">
	<analytic>
		<title level="a" type="main">Bridging the gap between natural language requirements and formal specifications</title>
		<author>
			<persName><surname>Bajwa</surname></persName>
		</author>
	</analytic>
	<monogr>
		<title level="m">Joint Proceedings of REFSQ-2016 Workshops, Doctoral Symposium, Research Method Track, and Poster Track co-located with the 22nd International Conference on Requirements Engineering: Foundation for Software Quality (REFSQ 2016)</title>
				<editor>
			<persName><forename type="first">Sanjai</forename><surname>Rayadurgam</surname></persName>
		</editor>
		<editor>
			<persName><forename type="first">Oksana</forename><surname>Tkachuk</surname></persName>
		</editor>
		<meeting><address><addrLine>Gothenburg, Sweden; Cham; Cham; Genoa, Italy</addrLine></address></meeting>
		<imprint>
			<publisher>ELRA</publisher>
			<date type="published" when="2001">2010. 2010. Oct 2010. 2012. 12 2012. 2016. March 14, 2016. 2016. 2014. 2014. 2016. 2016. 2001. 2001. 2014. 2014. 2006. May 2006</date>
			<biblScope unit="volume">10</biblScope>
			<biblScope unit="page" from="L06" to="1260" />
		</imprint>
	</monogr>
	<note>ACL Anthology Identifier</note>
</biblStruct>

<biblStruct xml:id="b1">
	<analytic>
		<title level="a" type="main">Petri nets: Properties, analysis and applications</title>
		<author>
			<persName><forename type="first">Tadao</forename><surname>Murata</surname></persName>
		</author>
		<author>
			<persName><surname>Murata</surname></persName>
		</author>
	</analytic>
	<monogr>
		<title level="m">Proceedings of the IEEE</title>
				<meeting>the IEEE</meeting>
		<imprint>
			<date type="published" when="1989-04">1989. April 1989</date>
			<biblScope unit="volume">77</biblScope>
			<biblScope unit="page" from="541" to="580" />
		</imprint>
	</monogr>
</biblStruct>

<biblStruct xml:id="b2">
	<analytic>
		<title level="a" type="main">The protege project: A look back and a look forward</title>
		<author>
			<persName><forename type="first">Mark</forename><forename type="middle">A</forename><surname>Musen</surname></persName>
		</author>
		<author>
			<persName><surname>Musen</surname></persName>
		</author>
	</analytic>
	<monogr>
		<title level="m">Franck Pommereau. Quickly prototyping Petri nets tools with SNAKES. Petri net newsletter</title>
				<imprint>
			<date type="published" when="1962">2015. June 2015. 1962. 1962. 2008. 10-2008. 10 2008</date>
			<biblScope unit="volume">1</biblScope>
			<biblScope unit="page" from="1" to="18" />
		</imprint>
		<respStmt>
			<orgName>Universitat Hamburg</orgName>
		</respStmt>
	</monogr>
	<note type="report_type">PhD thesis</note>
	<note>Pommereau</note>
</biblStruct>

<biblStruct xml:id="b3">
	<analytic>
		<title level="a" type="main">SNAKES: a flexible high-level Petri nets library</title>
		<author>
			<persName><forename type="first">Franck</forename><surname>Pommereau</surname></persName>
		</author>
		<author>
			<persName><surname>Pommereau</surname></persName>
		</author>
	</analytic>
	<monogr>
		<title level="m">Proceedings of Tenth International Workshop Modelling and Reasoning in Context (MRC) -13.07</title>
				<meeting>Tenth International Workshop Modelling and Reasoning in Context (MRC) -13.07<address><addrLine>Stockholm, Sweden</addrLine></address></meeting>
		<imprint>
			<date type="published" when="2015">2015. 2018. 9115</date>
			<biblScope unit="page" from="254" to="265" />
		</imprint>
	</monogr>
	<note>PETRI NETS&apos;15</note>
</biblStruct>

<biblStruct xml:id="b4">
	<analytic>
		<title level="a" type="main">Formalising natural language specifications using a cognitive linguistic/configuration based approach</title>
		<author>
			<persName><surname>Sadoun</surname></persName>
		</author>
	</analytic>
	<monogr>
		<title level="m">IEEE 25th International Conference on Tools with Artificial Intelligence</title>
				<editor>
			<persName><forename type="first">A</forename><surname>Leszek</surname></persName>
		</editor>
		<editor>
			<persName><forename type="first">Joaquim</forename><surname>Maciaszek</surname></persName>
		</editor>
		<editor>
			<persName><surname>Filipe</surname></persName>
		</editor>
		<meeting><address><addrLine>Cham</addrLine></address></meeting>
		<imprint>
			<publisher>Springer International Publishing</publisher>
			<date type="published" when="1998">2015. 2013. 2013. Nov 2013. 2015. 2015. Sept 2015. 2015. 1998. 1998. 2014. March 2014. 2016. 2016</date>
			<biblScope unit="volume">54</biblScope>
			<biblScope unit="page" from="1" to="20" />
		</imprint>
	</monogr>
	<note>Evaluation of Novel Approaches to Software Engineering</note>
</biblStruct>

<biblStruct xml:id="b5">
	<analytic>
		<title level="a" type="main">Formal consistency checking over specifications in natural languages</title>
		<author>
			<persName><forename type="first">Yan</forename></persName>
		</author>
	</analytic>
	<monogr>
		<title level="m">Tenth International Workshop Modelling and Reasoning in Context (MRC) -13.07</title>
				<meeting><address><addrLine>Stockholm, Sweden</addrLine></address></meeting>
		<imprint>
			<date type="published" when="2015-03">2015. March 2015</date>
			<biblScope unit="page">2018</biblScope>
		</imprint>
	</monogr>
	<note>2015 Design, Automation Test in Europe Conference Exhibition (DATE)</note>
</biblStruct>

				</listBibl>
			</div>
		</back>
	</text>
</TEI>
