Jove
Visualize
Contact Us
JoVE
x logofacebook logolinkedin logoyoutube logo
ABOUT JoVE
OverviewLeadershipBlogJoVE Help Center
AUTHORS
Publishing ProcessEditorial BoardScope & PoliciesPeer ReviewFAQSubmit
LIBRARIANS
TestimonialsSubscriptionsAccessResourcesLibrary Advisory BoardFAQ
RESEARCH
JoVE JournalMethods CollectionsJoVE Encyclopedia of ExperimentsArchive
EDUCATION
JoVE CoreJoVE BusinessJoVE Science EducationJoVE Lab ManualFaculty Resource CenterFaculty Site
Terms & Conditions of Use
Privacy Policy
Policies

Related Concept Videos

Methods of Documentation VI: Case Management Model01:15

Methods of Documentation VI: Case Management Model

791
The case management model is a multidisciplinary approach that involves healthcare professionals from diverse disciplines, such as physicians, nurses, therapists, social workers, and pharmacists, working collaboratively to address the various needs of patients. Each healthcare professional brings unique expertise and perspectives, contributing to a more comprehensive understanding of the patient's condition and tailoring treatment plans accordingly.
For example, a patient with a chronic...
791
Mechanistic Models: Overview of Compartment Models01:21

Mechanistic Models: Overview of Compartment Models

292
Mechanistic models, a category encompassing both physiological and compartmental modeling, differ from empirical models' approaches to incorporating known factors about the systems being modeled. Empirical models describe data with minimal assumptions, while mechanistic models aim to provide a robust description of available data by specifying assumptions and integrating known factors about the system. Compartmental analysis is a key example of a mechanistic model in pharmacokinetics and...
292
Modeling and Similitude01:12

Modeling and Similitude

535
Scaled modeling is a fundamental technique in engineering, enabling the study of large and complex systems by creating smaller, manageable replicas that recreate critical characteristics of the original. In hydrology and civil infrastructure, for example, scaled models of dams help analyze water flow, turbulence, and pressure. This method allows for accurate predictions of real-world behavior within a controlled environment, significantly reducing the cost and time involved in full-scale...
535
Mathematical Modeling: Problem Solving01:29

Mathematical Modeling: Problem Solving

183
Mathematical modeling transforms real-world scenarios into mathematical expressions, allowing for structured problem-solving and analysis. This process involves defining the situation, assigning variables to measurable quantities, selecting an appropriate model, and solving the resulting equation. Such models are invaluable in finance, providing precise methods to evaluate investments, loans, and repayment structures.A widely used example is the calculation of fixed monthly payments on a loan,...
183
Model Approaches for Pharmacokinetic Data: Compartment Models01:14

Model Approaches for Pharmacokinetic Data: Compartment Models

453
Compartmental analysis is a widely adopted approach to characterizing drug pharmacokinetics. It uses compartment models that conceptualize the body as a collection of reversibly communicating compartments, each representing a group of tissues exhibiting similar drug distribution characteristics. The movement rate of the drug between these compartments is typically described by first-order kinetics.
Two primary types of compartment models are recognized: mammillary and catenary. The more...
453
Mechanistic Models: Compartment Models in Algorithms for Numerical Problem Solving01:29

Mechanistic Models: Compartment Models in Algorithms for Numerical Problem Solving

228
Mechanistic models play a crucial role in algorithms for numerical problem-solving, particularly in nonlinear mixed effects modeling (NMEM). These models aim to minimize specific objective functions by evaluating various parameter estimates, leading to the development of systematic algorithms. In some cases, linearization techniques approximate the model using linear equations.
In individual population analyses, different algorithms are employed, such as Cauchy's method, which uses a...
228

You might also read

Related Articles

Articles linked to this work by shared authors, journal, and citation graph.

Sort by
Same author

Predicting the victims of hate speech on microblogging platforms.

Heliyon·2024
Same author

Measuring Effectiveness of Metamorphic Relations for Image Processing Using Mutation Testing.

Journal of imaging·2024
Same author

Evaluating the effectiveness of decomposed Halstead Metrics in software fault prediction.

PeerJ. Computer science·2023
Same author

Extraction of use case diagram elements using natural language processing and network science.

PloS one·2023
Same author

Green Synthesized Silver Nanoparticles: A Novel Approach for the Enhanced Growth and Yield of Tomato against Early Blight Disease.

Microorganisms·2023
Same author

Biogenic Synthesis, Characterization, and In Vitro Biological Evaluation of Silver Nanoparticles Using <i>Cleome brachycarpa</i>.

Plants (Basel, Switzerland)·2023

Related Experiment Video

Updated: Dec 23, 2025

Constructing and Visualizing Models using Mime-based Machine-learning Framework
06:19

Constructing and Visualizing Models using Mime-based Machine-learning Framework

Published on: July 22, 2025

2.0K

Formalizing the use case model: A model-based approach.

Qamar Uz Zaman1, Aamer Nadeem1, Muddassar Azam Sindhu2

  • 1Department of Computer Science, Capital University of Science and Technology (CUST), Islamabad, Pakistan.

Plos One
|April 21, 2020
PubMed
Summary
This summary is machine-generated.

This study presents an automated method to convert informal software requirements, like use cases, into formal specifications such as Kripke structures and Linear Temporal Logic (LTL). This reduces effort and enables early software behavior analysis.

More Related Videos

A Rapid Method for Modeling a Variable Cycle Engine
04:58

A Rapid Method for Modeling a Variable Cycle Engine

Published on: August 13, 2019

7.9K
A Modeling and Simulation Method for Preliminary Design of an Electro-Variable Displacement Pump
09:04

A Modeling and Simulation Method for Preliminary Design of an Electro-Variable Displacement Pump

Published on: June 1, 2022

3.4K

Related Experiment Videos

Last Updated: Dec 23, 2025

Constructing and Visualizing Models using Mime-based Machine-learning Framework
06:19

Constructing and Visualizing Models using Mime-based Machine-learning Framework

Published on: July 22, 2025

2.0K
A Rapid Method for Modeling a Variable Cycle Engine
04:58

A Rapid Method for Modeling a Variable Cycle Engine

Published on: August 13, 2019

7.9K
A Modeling and Simulation Method for Preliminary Design of an Electro-Variable Displacement Pump
09:04

A Modeling and Simulation Method for Preliminary Design of an Electro-Variable Displacement Pump

Published on: June 1, 2022

3.4K

Area of Science:

  • Software Engineering
  • Formal Methods
  • Requirements Engineering

Background:

  • Software development begins with natural language requirements documented as use cases.
  • Formalizing these requirements using notations like Linear Temporal Logic (LTL) or models like Kripke structures enhances rigor but demands significant time and expertise.
  • Existing conversion methods often require specialized skills or domain expert input, creating a need for automation.

Purpose of the Study:

  • To introduce an automated approach for transforming informal use case models into formal Kripke structures and LTL specifications.
  • To address the limitations of current methods that require extra skills or expert involvement.
  • To enable early analysis of software behavior and facilitate formal verification.

Main Methods:

  • Developed a template-based approach to accept use case models as input.
  • The approach automatically generates Kripke structures and LTL specifications, incorporating use case relationships (include, extend).
  • Utilized the NuSMV tool for verifying the generated LTL specifications against the Kripke structure model.

Main Results:

  • Successfully generated Kripke structures and LTL specifications from a SIM vending machine use case example.
  • Verification using NuSMV confirmed the validity of the generated specifications against the model, reporting no counterexamples.
  • The approach enables early software behavior analysis at the requirements stage.

Conclusions:

  • The proposed automated approach effectively converts informal use cases into formal Kripke structures and LTL specifications.
  • This method reduces the effort and expertise needed for formal requirement specification.
  • The early analysis and verification capabilities enhance the software development process.