List of Articles Formal Methods

• Open Access Article
  • Abstract Page
  • Full-Text
  
  1 - An Approach to Compose Viewpoints of Different Stakeholders in the Specification of Probabilistic Systems
  Mahboubeh Samadi haghighi haghighi
  10.7508/jist.2014.01.002
  Developing large and complex systems often involves many stakeholders each of which has her own expectations from the system; hence, it is difficult to write a single formal specification of the system considering all of stakeholders’ requirements at once; instead, each More

  Developing large and complex systems often involves many stakeholders each of which has her own expectations from the system; hence, it is difficult to write a single formal specification of the system considering all of stakeholders’ requirements at once; instead, each stakeholder can specify the system from her own viewpoint first. Then, the resulting specifications can be composed to prepare the final specification. Much work has been done so far for the specification of non-probabilistic systems regarding viewpoints (or expectations) of different stakeholders; however, because of big trend to apply formal methods on probabilistic systems, in this paper, we present an approach to compose viewpoints of different stakeholders in the specification of probabilistic systems. According to this approach, different viewpoints are separately specified using the Z notation. Then, the resulting specifications are composed using some new operators proposed in this paper. We show the applicability of the presented approach by performing it on a known case study. Manuscript profile
• Open Access Article
  • Abstract Page
  • Full-Text
  
  2 - A New Approach to the Quantitative Measurement of Software Reliability
  Abbas  Rasoolzadegan
  10.7508/jist.2015.03.005
  Nowadays software systems have very important role in a lot of sensitive and critical applications. Sometimes a small error in software could cause financial or even health loss in critical applications. So reliability assurance as a nun-functional requirement, is very More

  Nowadays software systems have very important role in a lot of sensitive and critical applications. Sometimes a small error in software could cause financial or even health loss in critical applications. So reliability assurance as a nun-functional requirement, is very vital.One of the key tasks to ensure error-free operation of the software, is to have a quantitative measurement of the software reliability.Software reliability engineering is defined as the quantitative study of the operational behavior of software systems with respect to user requirements concerning reliability. Software Reliability is defined as the probability of failure-free software operation for a specified period of time in a specified environment. Quantifying software reliability is increasingly becoming necessary. We have recently proposed a new approach (referred to as SDAFlex&Rel) to the development of «reliable yet flexible» software. In this paper, we first present the definitions of a set of key terms that are necessary to communicate with the scope and contributions of this work. Based on the fact that software reliability is directly proportional to the reliability of the development approach used, in this paper, a new approach is proposed to quantitatively measure the reliability of the software developed using SDAFlex&Rel, thereby making precise informal claims on the reliability improvement. The quantitative results confirm the reliability improvement that is informally promised by SDAFlex&Rel. Manuscript profile
• Open Access Article
  • Abstract Page
  • Full-Text
  
  3 - Determination of Formal Methods Capabilities for Software Specification and Analysis
  H. Banki V. Ahmadi Sabet
  Software developers face the problem of adopting a suitable formal method to developing their software. We aim to determine capability level of formal methods in software specification and analysis in four steps. The first step introduces the criteria by which the forma More

  Software developers face the problem of adopting a suitable formal method to developing their software. We aim to determine capability level of formal methods in software specification and analysis in four steps. The first step introduces the criteria by which the formal methods assess. The second and third ones deal with categorizing sorts of software and formal methods based on their solution methods. The fourth step determines fitness of some typical formal methods to specification and analysis of each software category. Manuscript profile