@article{4567,
  author = {Xiliang Nie, Hanxing Li},
  title = {A Formal Methodology for Multi Objective Run Time Requirement Enforcement on Many Core Systems Using FSMs},
  journal = {Digital Signal Processing and Artificial Intelligence for Automatic Learning},
  year = {2025},
  volume = {4},
  number = {3},
  doi = {https://doi.org/10.6025/dspaial/2025/4/3/113-125},
  url = {https://www.dline.info/dspai/fulltext/v4n3/dspaiv4n3_2.pdf},
  abstract = {The paper presents a methodology for multi objective run time requirement enforcement (RRE) on many core systems using finite state machines (FSMs). It addresses non functional requirements like latency and energy under varying workloads by modeling enforcement strategies as deterministic FSMs that adapt system configurations (e.g., voltage/frequency) based on feedback. The approach integrates a discrete time Markov chain (DTMC) to model environmental input variations and uses probabilistic computation tree logic (PCTL) for formal verification via the PRISM model checker. The authors evaluate five enforcement FSMs ranging from single requirement to multi requirement strategies on an image processing case study involving SIFT-based object detection.Verification goals assess the probability of violating latency, energy, or both requirements over consecutive executions. Results show trade offs between objectives: latency oriented strategies excel in timing but fail energetically, while balanced strategies like F3 perform best overall. The work highlights the need for systematic, formally verified design of enforcement mechanisms and proposes future automation for multi objective FSM synthesis.},
}