Welcome to pState

What is pState?

pState is experimental software toolkit under development for the design, validation and formal verification of complex systems. Classical statecharts are extended with probabilistic transitions, costs/rewards, and state invariants. Probabilistic choice can be used to model randomized algorithms or unreliable systems.

Relevant Publications

  1. Park, S., & Sekerinski, E. (2018). A Notebook Format for the Holistic Design of Embedded Systems (Tool Paper). In Electronic Proceedings in Theoretical Computer Science (Vol. 284). https://doi.org/10.4204/EPTCS.284.7 [pdf]
  2. Nokovic, B., & Sekerinski, E. (2017). Analysis and Implementation of Embedded System Models: Example of Tags in Item Management Application. In Model-Implementation Fidelity in Cyber Physical System Design (pp. 175–199). https://doi.org/10.1007/978-3-319-47307-9_7 [pdf]
  3. Nokovic, B., & Sekerinski, E. (2016). Automatically Quantitative Analysis and Code Generator for Sensor Systems: The Example of Great Lakes Water Quality Monitoring (Vol. 170, pp. 313–319). https://doi.org/10.1007/978-3-319-47075-7_35 [pdf]
  4. Nokovic, B., & Sekerinski, E. (2015). A Holistic Approach in Embedded System Development. In Electronic Proceedings in Theoretical Computer Science (Vol. 187). https://doi.org/10.4204/EPTCS.187.6 [pdf]
  5. Nokovic, B., & Sekerinski, E. (2014). Verification and Code Generation for Timed Transitions in pCharts. In ACM International Conference Proceeding Series. https://doi.org/10.1145/2641483.2641522 [pdf]
  6. Nokovic, B., & Sekerinski, E. (2013). pState: A probabilistic statecharts translator (pp. 29–32). https://doi.org/10.1109/MECO.2013.6601339 [pdf]
  7. Sekerinski, E. (2008). Verifying Statecharts with State Invariants. In Proceedings of the IEEE International Conference on Engineering of Complex Computer Systems, ICECCS (pp. 7–14). https://doi.org/10.1109/ICECCS.2008.40 [pdf]
  8. Sekerinski, E., & Zurob, R. (2001). iState: A Statechart Translator (Vol. 2185, pp. 376–390). https://doi.org/10.1007/3-540-45441-1_28 [pdf]